Metamath Proof Explorer

Theorem tususp

Description: A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 tuslem.k 
 |-  K = ( toUnifSp ` U )
2 id 
 |-  ( U e. ( UnifOn ` X ) -> U e. ( UnifOn ` X ) )
3 1 tususs 
 |-  ( U e. ( UnifOn ` X ) -> U = ( UnifSt ` K ) )
4 1 tusbas 
 |-  ( U e. ( UnifOn ` X ) -> X = ( Base ` K ) )
5 4 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( UnifOn ` X ) = ( UnifOn ` ( Base ` K ) ) )
6 2 3 5 3eltr3d 
 |-  ( U e. ( UnifOn ` X ) -> ( UnifSt ` K ) e. ( UnifOn ` ( Base ` K ) ) )
7 1 tusunif 
 |-  ( U e. ( UnifOn ` X ) -> U = ( UnifSet ` K ) )
8 7 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( unifTop ` ( UnifSet ` K ) ) )
9 1 tuslem 
 |-  ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) )
10 9 simp3d 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopOpen ` K ) )
11 7 3 eqtr3d 
 |-  ( U e. ( UnifOn ` X ) -> ( UnifSet ` K ) = ( UnifSt ` K ) )
12 11 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` ( UnifSet ` K ) ) = ( unifTop ` ( UnifSt ` K ) ) )
13 8 10 12 3eqtr3d 
 |-  ( U e. ( UnifOn ` X ) -> ( TopOpen ` K ) = ( unifTop ` ( UnifSt ` K ) ) )
14 eqid 
 |-  ( Base ` K ) = ( Base ` K )
15 eqid 
 |-  ( UnifSt ` K ) = ( UnifSt ` K )
16 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
17 14 15 16 isusp 
 |-  ( K e. UnifSp <-> ( ( UnifSt ` K ) e. ( UnifOn ` ( Base ` K ) ) /\ ( TopOpen ` K ) = ( unifTop ` ( UnifSt ` K ) ) ) )
18 6 13 17 sylanbrc 
 |-  ( U e. ( UnifOn ` X ) -> K e. UnifSp )