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 ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion uspreg ( ( 𝑊 ∈ UnifSp ∧ 𝐽 ∈ Haus ) → 𝐽 ∈ Reg )

Proof

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