Metamath Proof Explorer

Theorem tusbas

Description: The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 tuslem.k 
 |-  K = ( toUnifSp ` U )
2 1 tuslem 
 |-  ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) )
3 2 simp1d 
 |-  ( U e. ( UnifOn ` X ) -> X = ( Base ` K ) )