Theorem cplem2

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

	Ref	Expression
Hypothesis	cplem2.1	⊢ 𝐴 ∈ V
Assertion	cplem2	⊢ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝑦 ) ≠ ∅ )

Proof

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