Theorem cplem1

Description: Lemma for the Collection Principle cp . (Contributed by NM, 17-Oct-2003)

	Ref	Expression
Hypotheses	cplem1.1	$$⊢C=\left\{y\in B|\forall z\in B\mathrm{rank}\left(y\right)\subseteq \mathrm{rank}\left(z\right)\right\}$$
	cplem1.2	$$⊢D=\bigcup _{x\in A}C$$
Assertion	cplem1	$$⊢\forall x\in A\left(B\ne \varnothing \to B\cap D\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		cplem1.1	$$⊢C=\left\{y\in B|\forall z\in B\mathrm{rank}\left(y\right)\subseteq \mathrm{rank}\left(z\right)\right\}$$
2		cplem1.2	$$⊢D=\bigcup _{x\in A}C$$
3		scott0	$$⊢B=\varnothing \leftrightarrow \left\{y\in B|\forall z\in B\mathrm{rank}\left(y\right)\subseteq \mathrm{rank}\left(z\right)\right\}=\varnothing$$
4	1	eqeq1i	$$⊢C=\varnothing \leftrightarrow \left\{y\in B|\forall z\in B\mathrm{rank}\left(y\right)\subseteq \mathrm{rank}\left(z\right)\right\}=\varnothing$$
5	3 4	bitr4i	$$⊢B=\varnothing \leftrightarrow C=\varnothing$$
6	5	necon3bii	$$⊢B\ne \varnothing \leftrightarrow C\ne \varnothing$$
7		n0	$$⊢C\ne \varnothing \leftrightarrow \exists ww\in C$$
8	6 7	bitri	$$⊢B\ne \varnothing \leftrightarrow \exists ww\in C$$
9	1	ssrab3	$$⊢C\subseteq B$$
10	9	sseli	$$⊢w\in C\to w\in B$$
11	10	a1i	$$⊢x\in A\to \left(w\in C\to w\in B\right)$$
12		ssiun2	$$⊢x\in A\to C\subseteq \bigcup _{x\in A}C$$
13	12 2	sseqtrrdi	$$⊢x\in A\to C\subseteq D$$
14	13	sseld	$$⊢x\in A\to \left(w\in C\to w\in D\right)$$
15	11 14	jcad	$$⊢x\in A\to \left(w\in C\to \left(w\in B\wedge w\in D\right)\right)$$
16		inelcm	$$⊢\left(w\in B\wedge w\in D\right)\to B\cap D\ne \varnothing$$
17	15 16	syl6	$$⊢x\in A\to \left(w\in C\to B\cap D\ne \varnothing \right)$$
18	17	exlimdv	$$⊢x\in A\to \left(\exists ww\in C\to B\cap D\ne \varnothing \right)$$
19	8 18	biimtrid	$$⊢x\in A\to \left(B\ne \varnothing \to B\cap D\ne \varnothing \right)$$
20	19	rgen	$$⊢\forall x\in A\left(B\ne \varnothing \to B\cap D\ne \varnothing \right)$$