Metamath Proof Explorer

Theorem ishaus2

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

Ref Expression
Assertion ishaus2 ⊢ J ∈ TopOn ⁡ X → J ∈ Haus ↔ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
2 eqid ⊢ ⋃ J = ⋃ J
3 2 ishaus ⊢ J ∈ Haus ↔ J ∈ Top ∧ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
4 3 baib ⊢ J ∈ Top → J ∈ Haus ↔ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
5 1 4 syl ⊢ J ∈ TopOn ⁡ X → J ∈ Haus ↔ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
6 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
7 6 raleqdv ⊢ J ∈ TopOn ⁡ X → ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ ∀ y ∈ ⋃ J x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
8 6 7 raleqbidv ⊢ J ∈ TopOn ⁡ X → ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
9 5 8 bitr4d ⊢ J ∈ TopOn ⁡ X → J ∈ Haus ↔ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅