This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uspreg

Description: If a uniform space is Hausdorff, it is regular. Proposition 3 of BourbakiTop1 p. II.5. (Contributed by Thierry Arnoux, 4-Jan-2018)

Ref Expression
Hypothesis uspreg.1 ⊢ J = TopOpen ⁡ W
Assertion uspreg ⊢ W ∈ UnifSp ∧ J ∈ Haus → J ∈ Reg

Proof

Step Hyp Ref Expression
1 uspreg.1 ⊢ J = TopOpen ⁡ W
2 eqid ⊢ Base W = Base W
3 eqid ⊢ UnifSt ⁡ W = UnifSt ⁡ W
4 2 3 1 isusp ⊢ W ∈ UnifSp ↔ UnifSt ⁡ W ∈ UnifOn ⁡ Base W ∧ J = unifTop ⁡ UnifSt ⁡ W
5 4 simprbi ⊢ W ∈ UnifSp → J = unifTop ⁡ UnifSt ⁡ W
6 5 adantr ⊢ W ∈ UnifSp ∧ J ∈ Haus → J = unifTop ⁡ UnifSt ⁡ W
7 4 simplbi ⊢ W ∈ UnifSp → UnifSt ⁡ W ∈ UnifOn ⁡ Base W
8 simpr ⊢ W ∈ UnifSp ∧ J ∈ Haus → J ∈ Haus
9 6 8 eqeltrrd ⊢ W ∈ UnifSp ∧ J ∈ Haus → unifTop ⁡ UnifSt ⁡ W ∈ Haus
10 eqid ⊢ unifTop ⁡ UnifSt ⁡ W = unifTop ⁡ UnifSt ⁡ W
11 10 utopreg ⊢ UnifSt ⁡ W ∈ UnifOn ⁡ Base W ∧ unifTop ⁡ UnifSt ⁡ W ∈ Haus → unifTop ⁡ UnifSt ⁡ W ∈ Reg
12 7 9 11 syl2an2r ⊢ W ∈ UnifSp ∧ J ∈ Haus → unifTop ⁡ UnifSt ⁡ W ∈ Reg
13 6 12 eqeltrd ⊢ W ∈ UnifSp ∧ J ∈ Haus → J ∈ Reg