Metamath Proof Explorer

Theorem utopbas

Description: The base of the topology induced by a uniform structure U . (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Assertion utopbas 
|- ( U e. ( UnifOn ` X ) -> X = U. ( unifTop ` U ) )

Proof

Step Hyp Ref Expression
1 utopval 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } )
2 ssrab2 
 |-  { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } C_ ~P X
3 1 2 eqsstrdi 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) C_ ~P X )
4 ssidd 
 |-  ( U e. ( UnifOn ` X ) -> X C_ X )
5 ustssxp 
 |-  ( ( U e. ( UnifOn ` X ) /\ v e. U ) -> v C_ ( X X. X ) )
6 imassrn 
 |-  ( v " { x } ) C_ ran v
7 rnss 
 |-  ( v C_ ( X X. X ) -> ran v C_ ran ( X X. X ) )
8 rnxpid 
 |-  ran ( X X. X ) = X
9 7 8 sseqtrdi 
 |-  ( v C_ ( X X. X ) -> ran v C_ X )
10 6 9 sstrid 
 |-  ( v C_ ( X X. X ) -> ( v " { x } ) C_ X )
11 5 10 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ v e. U ) -> ( v " { x } ) C_ X )
12 11 ralrimiva 
 |-  ( U e. ( UnifOn ` X ) -> A. v e. U ( v " { x } ) C_ X )
13 ustne0 
 |-  ( U e. ( UnifOn ` X ) -> U =/= (/) )
14 r19.2zb 
 |-  ( U =/= (/) <-> ( A. v e. U ( v " { x } ) C_ X -> E. v e. U ( v " { x } ) C_ X ) )
15 13 14 sylib 
 |-  ( U e. ( UnifOn ` X ) -> ( A. v e. U ( v " { x } ) C_ X -> E. v e. U ( v " { x } ) C_ X ) )
16 12 15 mpd 
 |-  ( U e. ( UnifOn ` X ) -> E. v e. U ( v " { x } ) C_ X )
17 16 ralrimivw 
 |-  ( U e. ( UnifOn ` X ) -> A. x e. X E. v e. U ( v " { x } ) C_ X )
18 elutop 
 |-  ( U e. ( UnifOn ` X ) -> ( X e. ( unifTop ` U ) <-> ( X C_ X /\ A. x e. X E. v e. U ( v " { x } ) C_ X ) ) )
19 4 17 18 mpbir2and 
 |-  ( U e. ( UnifOn ` X ) -> X e. ( unifTop ` U ) )
20 elpwuni 
 |-  ( X e. ( unifTop ` U ) -> ( ( unifTop ` U ) C_ ~P X <-> U. ( unifTop ` U ) = X ) )
21 19 20 syl 
 |-  ( U e. ( UnifOn ` X ) -> ( ( unifTop ` U ) C_ ~P X <-> U. ( unifTop ` U ) = X ) )
22 3 21 mpbid 
 |-  ( U e. ( UnifOn ` X ) -> U. ( unifTop ` U ) = X )
23 22 eqcomd 
 |-  ( U e. ( UnifOn ` X ) -> X = U. ( unifTop ` U ) )