Metamath Proof Explorer

Theorem utopval

Description: The topology induced by a uniform structure U . (Contributed by Thierry Arnoux, 30-Nov-2017)

Ref Expression
Assertion utopval 
|- ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } )

Proof

Step Hyp Ref Expression
1 df-utop 
 |-  unifTop = ( u e. U. ran UnifOn |-> { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a } )
2 simpr 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> u = U )
3 2 unieqd 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> U. u = U. U )
4 3 dmeqd 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> dom U. u = dom U. U )
5 ustbas2 
 |-  ( U e. ( UnifOn ` X ) -> X = dom U. U )
6 5 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> X = dom U. U )
7 4 6 eqtr4d 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> dom U. u = X )
8 7 pweqd 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> ~P dom U. u = ~P X )
9 2 rexeqdv 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> ( E. v e. u ( v " { x } ) C_ a <-> E. v e. U ( v " { x } ) C_ a ) )
10 9 ralbidv 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> ( A. x e. a E. v e. u ( v " { x } ) C_ a <-> A. x e. a E. v e. U ( v " { x } ) C_ a ) )
11 8 10 rabeqbidv 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a } = { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } )
12 elrnust 
 |-  ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn )
13 elfvex 
 |-  ( U e. ( UnifOn ` X ) -> X e. _V )
14 pwexg 
 |-  ( X e. _V -> ~P X e. _V )
15 rabexg 
 |-  ( ~P X e. _V -> { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } e. _V )
16 13 14 15 3syl 
 |-  ( U e. ( UnifOn ` X ) -> { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } e. _V )
17 1 11 12 16 fvmptd2 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } )