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	⊢ 𝐴 ∈ V
Assertion	cplem2	⊢ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝑦 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		cplem2.1	⊢ 𝐴 ∈ V
2		scottex	⊢ Scott 𝐵 ∈ V
3	1 2	iunex	⊢ ∪ 𝑥 ∈ 𝐴 Scott 𝐵 ∈ V
4		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 Scott 𝐵
5	4	nfeq2	⊢ Ⅎ 𝑥 𝑦 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵
6		ineq2	⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵 → ( 𝐵 ∩ 𝑦 ) = ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 Scott 𝐵 ) )
7	6	neeq1d	⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵 → ( ( 𝐵 ∩ 𝑦 ) ≠ ∅ ↔ ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 Scott 𝐵 ) ≠ ∅ ) )
8	7	imbi2d	⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵 → ( ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝑦 ) ≠ ∅ ) ↔ ( 𝐵 ≠ ∅ → ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 Scott 𝐵 ) ≠ ∅ ) ) )
9	5 8	ralbid	⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝑦 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 Scott 𝐵 ) ≠ ∅ ) ) )
10		eqid	⊢ ∪ 𝑥 ∈ 𝐴 Scott 𝐵 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵
11	10	cplem1	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ ∪ 𝑥 ∈ 𝐴 Scott 𝐵 ) ≠ ∅ )
12	3 9 11	ceqsexv2d	⊢ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝑦 ) ≠ ∅ )