$( A \subseteq B \land B\subset C ) \implies (A \subset C) $ [ proof by quantification theory]

Question

I had a problem to find out the proper quantified sentence to prove this theorem. I saw an answer in this platform and here's the link. But I want to prove the theorem using only logic (I mean quantification theory). My approach is as follows:

$( A \subseteq B \land B\subset C ) \iff (\forall x)(x\in A \implies x\in B) \land (\forall x)(\exists y) ((x\in B\implies x\in C) \land (y\in C \land y\notin B)) \iff (\forall x)((x\in A \implies x\in B) \land (x\in B\implies x\in C)) \land (\exists y) (y\in C \land y\notin B) \implies (\forall x)(x\in A \implies x\in C) \land (\exists y) (y\in C \land y\notin B)$

Now, I just have to replace $(\exists y) (y\in C \land y\notin B)$ by $(\exists y) (y\in C \land y\notin A)$ from the existing information to complete the proof. This is where I got stuck. I, however, have the information that, $ A\subseteq B \iff (\forall y)(y\in A \implies y\in B)$ which is equivalent to, $ \neg (\exists y) \neg (y\in A \implies y\in B)$ which is also equivalent to, $ \neg (\exists y) (y\in A \land y\notin B)$. But this sentence isn't helpful to fulfill the replacement. So, how should I prove this sentence($(\exists y) (y\in C \land y\notin A)$). Any possibilities?

Another approach to the proof can be like this where I am also stuck. I mean I am actually confused whether my attempt is perfect mathematically or not. So, basically this approach is little bit more successful than the previous one.

$( A \subseteq B \land B\subset C ) \iff (A \subseteq B \land B\subseteq C \land B≠C) \iff (A \subseteq C \land B≠C) \iff ? $

Answer 1

Since you're struggling to see how to apply a universally quantified statement under an existential quantifier, let's prove that $(\forall x. P(x) \to Q(x)) \land (\exists y. P(y))$ implies $(\forall x. P(x) \to Q(x)) \land (\exists y. Q(y))$. In $\lambda$-calculus:

$$\lambda (f, y, p). (f, y, f(y, p))$$

Translating this into natural deduction gives something like:

1. assume $(\forall x. P(x) \to Q(x)) \land (\exists y. P(y))$
2. by 1 and left $\land$-elimination, $\forall x. P(x) \to Q(x)$
3. by 1 and right $\land$-elimination, $\exists y. P(y)$
4. by 3 and $\exists$-elimination, $P(y)$
5. by 2 and $\forall$-elimination, $P(y) \to Q(y)$
6. by 4, 5 and $\to$-elimination, $Q(y)$
7. by $\exists$-introduction, $\exists y. Q(y)$
8. by 2, 7 and $\land$-introduction, $(\forall x. P(x) \to Q(x)) \land (\exists y. Q(y))\ \square$

I will leave it up to you to adapt this to the statement you want to prove and the formal system you want to prove it in.

Elaborating on my comment, note that $\forall x. P(x) \to Q(x)$ does not imply $\exists x. P(x) \to Q(x)$: there might not be any $x$ at all (consider the empty set)! Instead, it implies $(\exists x. P(x)) \to (\exists x. Q(x))$, which is what we use here.

Answer 2

Another approach to the proof can be like this where I am also stuck. I mean I am actually confused whether my attempt is perfect mathematically or not. So, basically this approach is little bit more successful than the previous one.

$(A⊆B∧B⊂C)⟺(A⊆B∧B⊆C∧B≠C)⟺(A⊆C∧B≠C)⟺?$

Try $(A\subseteq B\wedge B\subset C) \iff ((A\subset B\vee A=B)\wedge B\subset C) ~~\ldots$

[This approach does not use quantification, although you may use it to construct a quantified proof.]