Metamath Proof Explorer


Theorem tustopn

Description: The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Hypotheses tuslem.k
|- K = ( toUnifSp ` U )
tustopn.j
|- J = ( unifTop ` U )
Assertion tustopn
|- ( U e. ( UnifOn ` X ) -> J = ( TopOpen ` K ) )

Proof

Step Hyp Ref Expression
1 tuslem.k
 |-  K = ( toUnifSp ` U )
2 tustopn.j
 |-  J = ( unifTop ` U )
3 1 tuslem
 |-  ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) )
4 3 simp3d
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopOpen ` K ) )
5 2 4 eqtrid
 |-  ( U e. ( UnifOn ` X ) -> J = ( TopOpen ` K ) )