Metamath Proof Explorer

Theorem hausnei

Description: Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007)

Ref Expression
Hypothesis ist0.1 ⊢ X = ⋃ J
Assertion hausnei ⊢ J ∈ Haus ∧ P ∈ X ∧ Q ∈ X ∧ P ≠ Q → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ X = ⋃ J
2 1 ishaus ⊢ J ∈ Haus ↔ J ∈ Top ∧ ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
3 2 simprbi ⊢ J ∈ Haus → ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
4 neeq1 ⊢ x = P → x ≠ y ↔ P ≠ y
5 eleq1 ⊢ x = P → x ∈ n ↔ P ∈ n
6 5 3anbi1d ⊢ x = P → x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ P ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
7 6 2rexbidv ⊢ x = P → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
8 4 7 imbi12d ⊢ x = P → x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ P ≠ y → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
9 neeq2 ⊢ y = Q → P ≠ y ↔ P ≠ Q
10 eleq1 ⊢ y = Q → y ∈ m ↔ Q ∈ m
11 10 3anbi2d ⊢ y = Q → P ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅
12 11 2rexbidv ⊢ y = Q → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅
13 9 12 imbi12d ⊢ y = Q → P ≠ y → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ ↔ P ≠ Q → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅
14 8 13 rspc2v ⊢ P ∈ X ∧ Q ∈ X → ∀ x ∈ X ∀ y ∈ X x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅ → P ≠ Q → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅
15 3 14 syl5 ⊢ P ∈ X ∧ Q ∈ X → J ∈ Haus → P ≠ Q → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅
16 15 ex ⊢ P ∈ X → Q ∈ X → J ∈ Haus → P ≠ Q → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅
17 16 com3r ⊢ J ∈ Haus → P ∈ X → Q ∈ X → P ≠ Q → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅
18 17 3imp2 ⊢ J ∈ Haus ∧ P ∈ X ∧ Q ∈ X ∧ P ≠ Q → ∃ n ∈ J ∃ m ∈ J P ∈ n ∧ Q ∈ m ∧ n ∩ m = ∅