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 ⊢ C = y ∈ B | ∀ z ∈ B rank ⁡ y ⊆ rank ⁡ z
cplem1.2 ⊢ D = ⋃ x ∈ A C
Assertion cplem1 ⊢ ∀ x ∈ A B ≠ ∅ → B ∩ D ≠ ∅

Proof

Step Hyp Ref Expression
1 cplem1.1 ⊢ C = y ∈ B | ∀ z ∈ B rank ⁡ y ⊆ rank ⁡ z
2 cplem1.2 ⊢ D = ⋃ x ∈ A C
3 scott0 ⊢ B = ∅ ↔ y ∈ B | ∀ z ∈ B rank ⁡ y ⊆ rank ⁡ z = ∅
4 1 eqeq1i ⊢ C = ∅ ↔ y ∈ B | ∀ z ∈ B rank ⁡ y ⊆ rank ⁡ z = ∅
5 3 4 bitr4i ⊢ B = ∅ ↔ C = ∅
6 5 necon3bii ⊢ B ≠ ∅ ↔ C ≠ ∅
7 n0 ⊢ C ≠ ∅ ↔ ∃ w w ∈ C
8 6 7 bitri ⊢ B ≠ ∅ ↔ ∃ w w ∈ C
9 1 ssrab3 ⊢ C ⊆ B
10 9 sseli ⊢ w ∈ C → w ∈ B
11 10 a1i ⊢ x ∈ A → w ∈ C → w ∈ B
12 ssiun2 ⊢ x ∈ A → C ⊆ ⋃ x ∈ A C
13 12 2 sseqtrrdi ⊢ x ∈ A → C ⊆ D
14 13 sseld ⊢ x ∈ A → w ∈ C → w ∈ D
15 11 14 jcad ⊢ x ∈ A → w ∈ C → w ∈ B ∧ w ∈ D
16 inelcm ⊢ w ∈ B ∧ w ∈ D → B ∩ D ≠ ∅
17 15 16 syl6 ⊢ x ∈ A → w ∈ C → B ∩ D ≠ ∅
18 17 exlimdv ⊢ x ∈ A → ∃ w w ∈ C → B ∩ D ≠ ∅
19 8 18 biimtrid ⊢ x ∈ A → B ≠ ∅ → B ∩ D ≠ ∅
20 19 rgen ⊢ ∀ x ∈ A B ≠ ∅ → B ∩ D ≠ ∅