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 e. UnifSp /\ J e. Haus ) -> J e. 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 e. UnifSp <-> ( ( UnifSt ` W ) e. ( UnifOn ` ( Base ` W ) ) /\ J = ( unifTop ` ( UnifSt ` W ) ) ) )
5 4 simprbi 
 |-  ( W e. UnifSp -> J = ( unifTop ` ( UnifSt ` W ) ) )
6 5 adantr 
 |-  ( ( W e. UnifSp /\ J e. Haus ) -> J = ( unifTop ` ( UnifSt ` W ) ) )
7 4 simplbi 
 |-  ( W e. UnifSp -> ( UnifSt ` W ) e. ( UnifOn ` ( Base ` W ) ) )
8 simpr 
 |-  ( ( W e. UnifSp /\ J e. Haus ) -> J e. Haus )
9 6 8 eqeltrrd 
 |-  ( ( W e. UnifSp /\ J e. Haus ) -> ( unifTop ` ( UnifSt ` W ) ) e. Haus )
10 eqid 
 |-  ( unifTop ` ( UnifSt ` W ) ) = ( unifTop ` ( UnifSt ` W ) )
11 10 utopreg 
 |-  ( ( ( UnifSt ` W ) e. ( UnifOn ` ( Base ` W ) ) /\ ( unifTop ` ( UnifSt ` W ) ) e. Haus ) -> ( unifTop ` ( UnifSt ` W ) ) e. Reg )
12 7 9 11 syl2an2r 
 |-  ( ( W e. UnifSp /\ J e. Haus ) -> ( unifTop ` ( UnifSt ` W ) ) e. Reg )
13 6 12 eqeltrd 
 |-  ( ( W e. UnifSp /\ J e. Haus ) -> J e. Reg )