Metamath Proof Explorer

Theorem utoptopon

Description: Topology induced by a uniform structure U with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018)

Ref Expression
Assertion utoptopon 
|- ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) e. ( TopOn ` X ) )

Proof

Step Hyp Ref Expression
1 utoptop 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) e. Top )
2 utopbas 
 |-  ( U e. ( UnifOn ` X ) -> X = U. ( unifTop ` U ) )
3 istopon 
 |-  ( ( unifTop ` U ) e. ( TopOn ` X ) <-> ( ( unifTop ` U ) e. Top /\ X = U. ( unifTop ` U ) ) )
4 1 2 3 sylanbrc 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) e. ( TopOn ` X ) )