Theorem cplem1

Description: Lemma for the Collection Principle cp . (Contributed by NM, 17-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026)

	Ref	Expression
Hypothesis	cplem1.1	$$⊢C=\bigcup _{x\in A}ScottB$$
Assertion	cplem1	$$⊢\forall x\in A\left(B\ne \varnothing \to B\cap C\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		cplem1.1	$$⊢C=\bigcup _{x\in A}ScottB$$
2		scott0b	$$⊢B=\varnothing \leftrightarrow ScottB=\varnothing$$
3	2	necon3bii	$$⊢B\ne \varnothing \leftrightarrow ScottB\ne \varnothing$$
4		n0	$$⊢ScottB\ne \varnothing \leftrightarrow \exists yy\in ScottB$$
5	3 4	bitri	$$⊢B\ne \varnothing \leftrightarrow \exists yy\in ScottB$$
6		scottss	$$⊢ScottB\subseteq B$$
7	6	sseli	$$⊢y\in ScottB\to y\in B$$
8	7	a1i	$$⊢x\in A\to \left(y\in ScottB\to y\in B\right)$$
9		ssiun2	$$⊢x\in A\to ScottB\subseteq \bigcup _{x\in A}ScottB$$
10	9 1	sseqtrrdi	$$⊢x\in A\to ScottB\subseteq C$$
11	10	sseld	$$⊢x\in A\to \left(y\in ScottB\to y\in C\right)$$
12	8 11	jcad	$$⊢x\in A\to \left(y\in ScottB\to \left(y\in B\wedge y\in C\right)\right)$$
13		inelcm	$$⊢\left(y\in B\wedge y\in C\right)\to B\cap C\ne \varnothing$$
14	12 13	syl6	$$⊢x\in A\to \left(y\in ScottB\to B\cap C\ne \varnothing \right)$$
15	14	exlimdv	$$⊢x\in A\to \left(\exists yy\in ScottB\to B\cap C\ne \varnothing \right)$$
16	5 15	biimtrid	$$⊢x\in A\to \left(B\ne \varnothing \to B\cap C\ne \varnothing \right)$$
17	16	rgen	$$⊢\forall x\in A\left(B\ne \varnothing \to B\cap C\ne \varnothing \right)$$