$$[(D\in C\implies D\in A)\implies (D\in C\implies D\in B)]\implies (D\in A\implies D\in B)$$

If you restore the quantifiers, this formula should be : $$[\forall C ,( \forall D, D\in C\implies D\in A)\implies (\forall D, D\in C\implies D\in B)]\implies (\forall D, D\in A\implies D\in B)$$

To prove that this implication holds, assume that : $$\forall C ,( \forall D, D\in C\implies D\in A)\implies (\forall D, D\in C\implies D\in B)$$ Then, since the LHS of the implication with $C$ replaced by $A$ : $$ \forall D, D\in A\implies D\in A$$ is true, the RHS must follow, and therefore : $$\forall D, D\in A\implies D\in B$$ which is what we wanted to prove.


  • But this is false, since it is not the case that $$[(D\in C\implies D\in A)\implies (D\in C\implies D\in B)]\implies (D\in A\implies D\in B)$$ https://www.umsu.de/trees/#((P~5Q)~5(P~5R))~5(Q~5R).

The claim is actually true. Notice that the left-hand side says $$[(C\subset A)\implies (C\subset B)],$$ while if $D\in A$, then $\{D\} \subset A$. Using the above, we get $\{D\}\subset B$, meaning $D\in B$.


You checked the formula

$$((P\rightarrow Q)\rightarrow (P\rightarrow R))\rightarrow (Q\rightarrow R)$$ using the "Tree Proof Generator"

https://www.umsu.de/trees/#((P~5Q)~5(P~5R))~5(Q~5R)

and got as result that the formula is invalid and

Countermodel:
P:  false
Q:  true
R:  false

But actually you wanted to check

$$[(D\in C\implies D\in A)\implies (D\in C\implies D\in B)]\implies (D\in A\implies D\in B) \tag 1$$

The "Tree Proof Generator" can handle predicates and a 1-ary predicate is a set. So you can translate your original question to an expression that can handled by the Tree Proof Generator. I use a lowercase $d$ instead of the uppercase $D$ to make this expression more readable.

$$( (Cd \to Ad ) \to (Cd \to Bd )) \to (Ad \to Bd ) $$

You can evaluate this by

https://www.umsu.de/trees/#((Cd~5Ad)~5(Cd~5Bd))~5(Ad~5Bd)

Again Tree Proof Generator tells you that the statement is invalid and returns

Countermodel:
Domain: { 0 }
d:  0
C:  { }
A:  { 0 }
B:  { }

Now one can see what is wrong with your statement. It is false if you choose these especial values for the variables.

$$((0 \in \emptyset \to 0 \in \{0\}) \to (0 \in \emptyset \to 0 \in \emptyset)) \to (0 \in \{0\} \to 0 \in \emptyset) $$

But that is not what you wanted to claim with $(1)$. The $d$ in all paranthese expressions should not be the same. We need the $\forall$ quantor:

$$( \forall d (Cd \to Ad ) \to \forall d (Cd \to Bd )) \to \forall d (Ad \to Bd ) $$

Note that this is the same as to

$$( \forall x (Cx \to Ax ) \to \forall y (Cy \to By )) \to \forall z (Az \to Bz ) \tag 3$$

We can put this in the Tree Proof Generator

https://www.umsu.de/trees/#(~6d(Cd~5Ad)~5~6d(Cd~5Bd))~5~6d(Ad~5Bd)

We get still the message that this is an invalid statement and the output

Countermodel:
Domain: { 0 }
C:  { }
A:  { 0 }
B:  { }

We note that $(3)$ this is still not what we want to say. We want not restrict to a special $C$, but the left hand side of the main implication should be true for all sets $C$, not only for one $C$. So we finally get this expressen

$$(\forall C( \forall d (Cd \to Ad ) \to \forall d (Cd \to Bd ))) \to \forall d (Ad \to Bd ) $$

This we cannot proof with the Tree Proof Generator because it cannot handle predicates in quantors. But $(4)$ is true as SolubleFish has already proved here.