Metamath Proof Explorer

Theorem neiptopreu

Description: If, to each element P of a set X , we associate a set ( NP ) fulfilling Properties V_i, V_ii, V_iii and Property V_iv of BourbakiTop1 p. I.2. , corresponding to ssnei , innei , elnei and neissex , then there is a unique topology j such that for any point p , ( Np ) is the set of neighborhoods of p . Proposition 2 of BourbakiTop1 p. I.3. This can be used to build a topology from a set of neighborhoods. Note that innei uses binary intersections whereas Property V_ii mentions finite intersections (which includes the empty intersection of subsets of X , which is equal to X ), so we add the hypothesis that X is a neighborhood of all points. TODO: when df-fi includes the empty intersection, remove that extra hypothesis. (Contributed by Thierry Arnoux, 6-Jan-2018)

Ref Expression
Hypotheses neiptop.o 
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }
neiptop.0 
|- ( ph -> N : X --> ~P ~P X )
neiptop.1 
|- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
neiptop.2 
|- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
neiptop.3 
|- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
neiptop.4 
|- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
neiptop.5 
|- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )
Assertion neiptopreu 
|- ( ph -> E! j e. ( TopOn ` X ) N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )

Proof

Step Hyp Ref Expression
1 neiptop.o 
 |-  J = { a e. ~P X | A. p e. a a e. ( N ` p ) }
2 neiptop.0 
 |-  ( ph -> N : X --> ~P ~P X )
3 neiptop.1 
 |-  ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
4 neiptop.2 
 |-  ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
5 neiptop.3 
 |-  ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
6 neiptop.4 
 |-  ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
7 neiptop.5 
 |-  ( ( ph /\ p e. X ) -> X e. ( N ` p ) )
8 1 2 3 4 5 6 7 neiptoptop 
 |-  ( ph -> J e. Top )
9 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
10 8 9 sylib 
 |-  ( ph -> J e. ( TopOn ` U. J ) )
11 1 2 3 4 5 6 7 neiptopuni 
 |-  ( ph -> X = U. J )
12 11 fveq2d 
 |-  ( ph -> ( TopOn ` X ) = ( TopOn ` U. J ) )
13 10 12 eleqtrrd 
 |-  ( ph -> J e. ( TopOn ` X ) )
14 1 2 3 4 5 6 7 neiptopnei 
 |-  ( ph -> N = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) )
15 nfv 
 |-  F/ p ( ph /\ j e. ( TopOn ` X ) )
16 nfmpt1 
 |-  F/_ p ( p e. X |-> ( ( nei ` j ) ` { p } ) )
17 16 nfeq2 
 |-  F/ p N = ( p e. X |-> ( ( nei ` j ) ` { p } ) )
18 15 17 nfan 
 |-  F/ p ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )
19 nfv 
 |-  F/ p b C_ X
20 18 19 nfan 
 |-  F/ p ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b C_ X )
21 simpllr 
 |-  ( ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b C_ X ) /\ p e. b ) -> N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )
22 simpr 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b C_ X ) -> b C_ X )
23 22 sselda 
 |-  ( ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b C_ X ) /\ p e. b ) -> p e. X )
24 id 
 |-  ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) -> N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )
25 fvexd 
 |-  ( ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) /\ p e. X ) -> ( ( nei ` j ) ` { p } ) e. _V )
26 24 25 fvmpt2d 
 |-  ( ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) /\ p e. X ) -> ( N ` p ) = ( ( nei ` j ) ` { p } ) )
27 21 23 26 syl2anc 
 |-  ( ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b C_ X ) /\ p e. b ) -> ( N ` p ) = ( ( nei ` j ) ` { p } ) )
28 27 eqcomd 
 |-  ( ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b C_ X ) /\ p e. b ) -> ( ( nei ` j ) ` { p } ) = ( N ` p ) )
29 28 eleq2d 
 |-  ( ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b C_ X ) /\ p e. b ) -> ( b e. ( ( nei ` j ) ` { p } ) <-> b e. ( N ` p ) ) )
30 20 29 ralbida 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b C_ X ) -> ( A. p e. b b e. ( ( nei ` j ) ` { p } ) <-> A. p e. b b e. ( N ` p ) ) )
31 30 pm5.32da 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) -> ( ( b C_ X /\ A. p e. b b e. ( ( nei ` j ) ` { p } ) ) <-> ( b C_ X /\ A. p e. b b e. ( N ` p ) ) ) )
32 toponss 
 |-  ( ( j e. ( TopOn ` X ) /\ b e. j ) -> b C_ X )
33 32 ad4ant24 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b e. j ) -> b C_ X )
34 topontop 
 |-  ( j e. ( TopOn ` X ) -> j e. Top )
35 34 ad2antlr 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) -> j e. Top )
36 opnnei 
 |-  ( j e. Top -> ( b e. j <-> A. p e. b b e. ( ( nei ` j ) ` { p } ) ) )
37 35 36 syl 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) -> ( b e. j <-> A. p e. b b e. ( ( nei ` j ) ` { p } ) ) )
38 37 biimpa 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b e. j ) -> A. p e. b b e. ( ( nei ` j ) ` { p } ) )
39 33 38 jca 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ b e. j ) -> ( b C_ X /\ A. p e. b b e. ( ( nei ` j ) ` { p } ) ) )
40 37 biimpar 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ A. p e. b b e. ( ( nei ` j ) ` { p } ) ) -> b e. j )
41 40 adantrl 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) /\ ( b C_ X /\ A. p e. b b e. ( ( nei ` j ) ` { p } ) ) ) -> b e. j )
42 39 41 impbida 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) -> ( b e. j <-> ( b C_ X /\ A. p e. b b e. ( ( nei ` j ) ` { p } ) ) ) )
43 1 neipeltop 
 |-  ( b e. J <-> ( b C_ X /\ A. p e. b b e. ( N ` p ) ) )
44 43 a1i 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) -> ( b e. J <-> ( b C_ X /\ A. p e. b b e. ( N ` p ) ) ) )
45 31 42 44 3bitr4d 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) -> ( b e. j <-> b e. J ) )
46 45 eqrdv 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) ) -> j = J )
47 46 ex 
 |-  ( ( ph /\ j e. ( TopOn ` X ) ) -> ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) -> j = J ) )
48 47 ralrimiva 
 |-  ( ph -> A. j e. ( TopOn ` X ) ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) -> j = J ) )
49 simpl 
 |-  ( ( j = J /\ p e. X ) -> j = J )
50 49 fveq2d 
 |-  ( ( j = J /\ p e. X ) -> ( nei ` j ) = ( nei ` J ) )
51 50 fveq1d 
 |-  ( ( j = J /\ p e. X ) -> ( ( nei ` j ) ` { p } ) = ( ( nei ` J ) ` { p } ) )
52 51 mpteq2dva 
 |-  ( j = J -> ( p e. X |-> ( ( nei ` j ) ` { p } ) ) = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) )
53 52 eqeq2d 
 |-  ( j = J -> ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) <-> N = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) ) )
54 53 eqreu 
 |-  ( ( J e. ( TopOn ` X ) /\ N = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) /\ A. j e. ( TopOn ` X ) ( N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) -> j = J ) ) -> E! j e. ( TopOn ` X ) N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )
55 13 14 48 54 syl3anc 
 |-  ( ph -> E! j e. ( TopOn ` X ) N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )