This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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