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

Metamath Proof Explorer

Theorem cplem1

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

Ref Expression
Hypotheses cplem1.1 ⊢ 𝐶 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) }
cplem1.2 ⊢ 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶
Assertion cplem1 ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐷 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 cplem1.1 ⊢ 𝐶 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) }
2 cplem1.2 ⊢ 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶
3 scott0 ⊢ ( 𝐵 = ∅ ↔ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) } = ∅ )
4 1 eqeq1i ⊢ ( 𝐶 = ∅ ↔ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) } = ∅ )
5 3 4 bitr4i ⊢ ( 𝐵 = ∅ ↔ 𝐶 = ∅ )
6 5 necon3bii ⊢ ( 𝐵 ≠ ∅ ↔ 𝐶 ≠ ∅ )
7 n0 ⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐶 )
8 6 7 bitri ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐶 )
9 1 ssrab3 ⊢ 𝐶 ⊆ 𝐵
10 9 sseli ⊢ ( 𝑤 ∈ 𝐶 → 𝑤 ∈ 𝐵 )
11 10 a1i ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐶 → 𝑤 ∈ 𝐵 ) )
12 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 )
13 12 2 sseqtrrdi ⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ⊆ 𝐷 )
14 13 sseld ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐶 → 𝑤 ∈ 𝐷 ) )
15 11 14 jcad ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐶 → ( 𝑤 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) ) )
16 inelcm ⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) → ( 𝐵 ∩ 𝐷 ) ≠ ∅ )
17 15 16 syl6 ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐶 → ( 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
18 17 exlimdv ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑤 𝑤 ∈ 𝐶 → ( 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
19 8 18 biimtrid ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
20 19 rgen ⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐷 ) ≠ ∅ )