Metamath Proof Explorer

Theorem ustuqtop

Description: For a given uniform structure U on a set X , there is a unique topology j such that the set ran ( v e. U |-> ( v " { p } ) ) is the filter of the neighborhoods of p for that topology. Proposition 1 of BourbakiTop1 p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018)

Ref Expression
Hypothesis utopustuq.1 
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
Assertion ustuqtop 
|- ( U e. ( UnifOn ` X ) -> E! j e. ( TopOn ` X ) A. p e. X ( N ` p ) = ( ( nei ` j ) ` { p } ) )

Proof

Step Hyp Ref Expression
1 utopustuq.1 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2 fveq2 
 |-  ( p = r -> ( N ` p ) = ( N ` r ) )
3 2 eleq2d 
 |-  ( p = r -> ( c e. ( N ` p ) <-> c e. ( N ` r ) ) )
4 3 cbvralvw 
 |-  ( A. p e. c c e. ( N ` p ) <-> A. r e. c c e. ( N ` r ) )
5 eleq1w 
 |-  ( c = a -> ( c e. ( N ` p ) <-> a e. ( N ` p ) ) )
6 5 raleqbi1dv 
 |-  ( c = a -> ( A. p e. c c e. ( N ` p ) <-> A. p e. a a e. ( N ` p ) ) )
7 4 6 bitr3id 
 |-  ( c = a -> ( A. r e. c c e. ( N ` r ) <-> A. p e. a a e. ( N ` p ) ) )
8 7 cbvrabv 
 |-  { c e. ~P X | A. r e. c c e. ( N ` r ) } = { a e. ~P X | A. p e. a a e. ( N ` p ) }
9 1 ustuqtop0 
 |-  ( U e. ( UnifOn ` X ) -> N : X --> ~P ~P X )
10 1 ustuqtop1 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
11 1 ustuqtop2 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
12 1 ustuqtop3 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
13 1 ustuqtop4 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. x e. b a e. ( N ` x ) )
14 1 ustuqtop5 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> X e. ( N ` p ) )
15 8 9 10 11 12 13 14 neiptopreu 
 |-  ( U e. ( UnifOn ` X ) -> E! j e. ( TopOn ` X ) N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )
16 9 feqmptd 
 |-  ( U e. ( UnifOn ` X ) -> N = ( p e. X |-> ( N ` p ) ) )
17 16 eqeq1d 
 |-  ( U e. ( UnifOn ` X ) -> ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) <-> ( p e. X |-> ( N ` p ) ) = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) )
18 fvex 
 |-  ( N ` p ) e. _V
19 18 rgenw 
 |-  A. p e. X ( N ` p ) e. _V
20 mpteqb 
 |-  ( A. p e. X ( N ` p ) e. _V -> ( ( p e. X |-> ( N ` p ) ) = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) <-> A. p e. X ( N ` p ) = ( ( nei ` j ) ` { p } ) ) )
21 19 20 ax-mp 
 |-  ( ( p e. X |-> ( N ` p ) ) = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) <-> A. p e. X ( N ` p ) = ( ( nei ` j ) ` { p } ) )
22 17 21 bitrdi 
 |-  ( U e. ( UnifOn ` X ) -> ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) <-> A. p e. X ( N ` p ) = ( ( nei ` j ) ` { p } ) ) )
23 22 reubidv 
 |-  ( U e. ( UnifOn ` X ) -> ( E! j e. ( TopOn ` X ) N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) <-> E! j e. ( TopOn ` X ) A. p e. X ( N ` p ) = ( ( nei ` j ) ` { p } ) ) )
24 15 23 mpbid 
 |-  ( U e. ( UnifOn ` X ) -> E! j e. ( TopOn ` X ) A. p e. X ( N ` p ) = ( ( nei ` j ) ` { p } ) )