Theorem cplem2

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	cplem2.1	$$⊢A\in \mathrm{V}$$
Assertion	cplem2	$$⊢\exists y\forall x\in A\left(B\ne \varnothing \to B\cap y\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		cplem2.1	$$⊢A\in \mathrm{V}$$
2		scottex	$$⊢ScottB\in \mathrm{V}$$
3	1 2	iunex	$$⊢\bigcup _{x\in A}ScottB\in \mathrm{V}$$
4		nfiu1	$$⊢\underset{\_}{Ⅎ}x\bigcup _{x\in A}ScottB$$
5	4	nfeq2	$$⊢Ⅎxy=\bigcup _{x\in A}ScottB$$
6		ineq2	$$⊢y=\bigcup _{x\in A}ScottB\to B\cap y=B\cap \bigcup _{x\in A}ScottB$$
7	6	neeq1d	$$⊢y=\bigcup _{x\in A}ScottB\to \left(B\cap y\ne \varnothing \leftrightarrow B\cap \bigcup _{x\in A}ScottB\ne \varnothing \right)$$
8	7	imbi2d	$$⊢y=\bigcup _{x\in A}ScottB\to \left(\left(B\ne \varnothing \to B\cap y\ne \varnothing \right)\leftrightarrow \left(B\ne \varnothing \to B\cap \bigcup _{x\in A}ScottB\ne \varnothing \right)\right)$$
9	5 8	ralbid	$$⊢y=\bigcup _{x\in A}ScottB\to \left(\forall x\in A\left(B\ne \varnothing \to B\cap y\ne \varnothing \right)\leftrightarrow \forall x\in A\left(B\ne \varnothing \to B\cap \bigcup _{x\in A}ScottB\ne \varnothing \right)\right)$$
10		eqid	$$⊢\bigcup _{x\in A}ScottB=\bigcup _{x\in A}ScottB$$
11	10	cplem1	$$⊢\forall x\in A\left(B\ne \varnothing \to B\cap \bigcup _{x\in A}ScottB\ne \varnothing \right)$$
12	3 9 11	ceqsexv2d	$$⊢\exists y\forall x\in A\left(B\ne \varnothing \to B\cap y\ne \varnothing \right)$$