Metamath Proof Explorer

Theorem cplem2

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

Ref Expression
Hypothesis cplem2.1 ⊢ A ∈ V
Assertion cplem2 ⊢ ∃ y ∀ x ∈ A B ≠ ∅ → B ∩ y ≠ ∅

Proof

Step Hyp Ref Expression
1 cplem2.1 ⊢ A ∈ V
2 scottex ⊢ z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w ∈ V
3 1 2 iunex ⊢ ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w ∈ V
4 nfiu1 ⊢ Ⅎ _ x ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w
5 4 nfeq2 ⊢ Ⅎ x y = ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w
6 ineq2 ⊢ y = ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w → B ∩ y = B ∩ ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w
7 6 neeq1d ⊢ y = ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w → B ∩ y ≠ ∅ ↔ B ∩ ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w ≠ ∅
8 7 imbi2d ⊢ y = ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w → B ≠ ∅ → B ∩ y ≠ ∅ ↔ B ≠ ∅ → B ∩ ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w ≠ ∅
9 5 8 ralbid ⊢ y = ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w → ∀ x ∈ A B ≠ ∅ → B ∩ y ≠ ∅ ↔ ∀ x ∈ A B ≠ ∅ → B ∩ ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w ≠ ∅
10 eqid ⊢ z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w = z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w
11 eqid ⊢ ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w = ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w
12 10 11 cplem1 ⊢ ∀ x ∈ A B ≠ ∅ → B ∩ ⋃ x ∈ A z ∈ B | ∀ w ∈ B rank ⁡ z ⊆ rank ⁡ w ≠ ∅
13 3 9 12 ceqsexv2d ⊢ ∃ y ∀ x ∈ A B ≠ ∅ → B ∩ y ≠ ∅