Metamath Proof Explorer

Theorem tustps

Description: A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018)

Ref Expression
Hypothesis tuslem.k 
|- K = ( toUnifSp ` U )
Assertion tustps 
|- ( U e. ( UnifOn ` X ) -> K e. TopSp )

Proof

Step Hyp Ref Expression
1 tuslem.k 
 |-  K = ( toUnifSp ` U )
2 utoptopon 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) e. ( TopOn ` X ) )
3 eqid 
 |-  ( unifTop ` U ) = ( unifTop ` U )
4 1 3 tustopn 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopOpen ` K ) )
5 1 tusbas 
 |-  ( U e. ( UnifOn ` X ) -> X = ( Base ` K ) )
6 5 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( TopOn ` X ) = ( TopOn ` ( Base ` K ) ) )
7 2 4 6 3eltr3d 
 |-  ( U e. ( UnifOn ` X ) -> ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
10 8 9 istps 
 |-  ( K e. TopSp <-> ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) )
11 7 10 sylibr 
 |-  ( U e. ( UnifOn ` X ) -> K e. TopSp )