Metamath Proof Explorer

Theorem ishaus

Description: The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007)

Ref Expression
Hypothesis ist0.1 ⊢ X = ⋃ J
Assertion ishaus ⊢ J ∈ Haus ↔ J ∈ Top ∧ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ X = ⋃ J
2 unieq ⊢ j = J → ⋃ j = ⋃ J
3 2 1 eqtr4di ⊢ j = J → ⋃ j = X
4 rexeq ⊢ j = J → ∃ m ∈ j x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
5 4 rexeqbi1dv ⊢ j = J → ∃ n ∈ j ∃ m ∈ j x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
6 5 imbi2d ⊢ j = J → x ≠ y → ∃ n ∈ j ∃ m ∈ j x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
7 3 6 raleqbidv ⊢ j = J → ∀ y ∈ ⋃ j x ≠ y → ∃ n ∈ j ∃ m ∈ j x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
8 3 7 raleqbidv ⊢ j = J → ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j x ≠ y → ∃ n ∈ j ∃ m ∈ j x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
9 df-haus ⊢ Haus = j ∈ Top | ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j x ≠ y → ∃ n ∈ j ∃ m ∈ j x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
10 8 9 elrab2 ⊢ J ∈ Haus ↔ J ∈ Top ∧ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅