Metamath Proof Explorer

Theorem cplem2OLD

Description: Obsolete version of cplem2 as of 19-Jul-2026. (Contributed by NM, 17-Oct-2003) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cplem2OLD.1 ⊢ A ∈ V
2 scottexOLD ⊢ 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 cplem1OLD ⊢ ∀ 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 ≠ ∅