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 } ) ) )