Metamath Proof Explorer


Theorem utopsnneiplem

Description: The neighborhoods of a point P for the topology induced by an uniform space U . (Contributed by Thierry Arnoux, 11-Jan-2018)

Ref Expression
Hypotheses utoptop.1 J=unifTopU
utopsnneip.1 K=a𝒫X|paaNp
utopsnneip.2 N=pXranvUvp
Assertion utopsnneiplem UUnifOnXPXneiJP=ranvUvP

Proof

Step Hyp Ref Expression
1 utoptop.1 J=unifTopU
2 utopsnneip.1 K=a𝒫X|paaNp
3 utopsnneip.2 N=pXranvUvp
4 utopval UUnifOnXunifTopU=a𝒫X|pawUwpa
5 1 4 eqtrid UUnifOnXJ=a𝒫X|pawUwpa
6 simpll UUnifOnXa𝒫XpaUUnifOnX
7 simpr UUnifOnXa𝒫Xa𝒫X
8 7 elpwid UUnifOnXa𝒫XaX
9 8 sselda UUnifOnXa𝒫XpapX
10 simpr UUnifOnXpXpX
11 mptexg UUnifOnXvUvpV
12 rnexg vUvpVranvUvpV
13 11 12 syl UUnifOnXranvUvpV
14 13 adantr UUnifOnXpXranvUvpV
15 3 fvmpt2 pXranvUvpVNp=ranvUvp
16 10 14 15 syl2anc UUnifOnXpXNp=ranvUvp
17 16 eleq2d UUnifOnXpXaNparanvUvp
18 eqid vUvp=vUvp
19 18 elrnmpt aVaranvUvpvUa=vp
20 19 elv aranvUvpvUa=vp
21 17 20 bitrdi UUnifOnXpXaNpvUa=vp
22 6 9 21 syl2anc UUnifOnXa𝒫XpaaNpvUa=vp
23 nfv vUUnifOnXa𝒫Xpa
24 nfre1 vvUa=vp
25 23 24 nfan vUUnifOnXa𝒫XpavUa=vp
26 simplr UUnifOnXa𝒫XpavUa=vpvUa=vpvU
27 eqimss2 a=vpvpa
28 27 adantl UUnifOnXa𝒫XpavUa=vpvUa=vpvpa
29 imaeq1 w=vwp=vp
30 29 sseq1d w=vwpavpa
31 30 rspcev vUvpawUwpa
32 26 28 31 syl2anc UUnifOnXa𝒫XpavUa=vpvUa=vpwUwpa
33 simpr UUnifOnXa𝒫XpavUa=vpvUa=vp
34 25 32 33 r19.29af UUnifOnXa𝒫XpavUa=vpwUwpa
35 6 ad2antrr UUnifOnXa𝒫XpawUwpaUUnifOnX
36 9 ad2antrr UUnifOnXa𝒫XpawUwpapX
37 35 36 jca UUnifOnXa𝒫XpawUwpaUUnifOnXpX
38 simpr UUnifOnXa𝒫XpawUwpawpa
39 8 ad3antrrr UUnifOnXa𝒫XpawUwpaaX
40 simplr UUnifOnXa𝒫XpawUwpawU
41 eqid wp=wp
42 imaeq1 u=wup=wp
43 42 rspceeqv wUwp=wpuUwp=up
44 41 43 mpan2 wUuUwp=up
45 44 adantl UUnifOnXpXwUuUwp=up
46 vex wV
47 46 imaex wpV
48 3 ustuqtoplem UUnifOnXpXwpVwpNpuUwp=up
49 47 48 mpan2 UUnifOnXpXwpNpuUwp=up
50 49 adantr UUnifOnXpXwUwpNpuUwp=up
51 45 50 mpbird UUnifOnXpXwUwpNp
52 35 36 40 51 syl21anc UUnifOnXa𝒫XpawUwpawpNp
53 sseq1 b=wpbawpa
54 53 3anbi2d b=wpUUnifOnXpXbaaXUUnifOnXpXwpaaX
55 eleq1 b=wpbNpwpNp
56 54 55 anbi12d b=wpUUnifOnXpXbaaXbNpUUnifOnXpXwpaaXwpNp
57 56 imbi1d b=wpUUnifOnXpXbaaXbNpaNpUUnifOnXpXwpaaXwpNpaNp
58 3 ustuqtop1 UUnifOnXpXbaaXbNpaNp
59 47 57 58 vtocl UUnifOnXpXwpaaXwpNpaNp
60 37 38 39 52 59 syl31anc UUnifOnXa𝒫XpawUwpaaNp
61 37 21 syl UUnifOnXa𝒫XpawUwpaaNpvUa=vp
62 60 61 mpbid UUnifOnXa𝒫XpawUwpavUa=vp
63 62 r19.29an UUnifOnXa𝒫XpawUwpavUa=vp
64 34 63 impbida UUnifOnXa𝒫XpavUa=vpwUwpa
65 22 64 bitrd UUnifOnXa𝒫XpaaNpwUwpa
66 65 ralbidva UUnifOnXa𝒫XpaaNppawUwpa
67 66 rabbidva UUnifOnXa𝒫X|paaNp=a𝒫X|pawUwpa
68 5 67 eqtr4d UUnifOnXJ=a𝒫X|paaNp
69 68 2 eqtr4di UUnifOnXJ=K
70 69 fveq2d UUnifOnXneiJ=neiK
71 70 fveq1d UUnifOnXneiJP=neiKP
72 71 adantr UUnifOnXPXneiJP=neiKP
73 3 ustuqtop0 UUnifOnXN:X𝒫𝒫X
74 3 ustuqtop1 UUnifOnXpXabbXaNpbNp
75 3 ustuqtop2 UUnifOnXpXfiNpNp
76 3 ustuqtop3 UUnifOnXpXaNppa
77 3 ustuqtop4 UUnifOnXpXaNpbNpqbaNq
78 3 ustuqtop5 UUnifOnXpXXNp
79 2 73 74 75 76 77 78 neiptopnei UUnifOnXN=pXneiKp
80 79 adantr UUnifOnXPXN=pXneiKp
81 simpr UUnifOnXPXp=Pp=P
82 81 sneqd UUnifOnXPXp=Pp=P
83 82 fveq2d UUnifOnXPXp=PneiKp=neiKP
84 simpr UUnifOnXPXPX
85 fvexd UUnifOnXPXneiKPV
86 80 83 84 85 fvmptd UUnifOnXPXNP=neiKP
87 mptexg UUnifOnXvUvPV
88 rnexg vUvPVranvUvPV
89 87 88 syl UUnifOnXranvUvPV
90 89 adantr UUnifOnXPXranvUvPV
91 nfv vPX
92 nfmpt1 _vvUvP
93 92 nfrn _vranvUvP
94 93 nfel1 vranvUvPV
95 91 94 nfan vPXranvUvPV
96 nfv vp=P
97 95 96 nfan vPXranvUvPVp=P
98 simpr2 PXranvUvPVp=PvUp=P
99 98 sneqd PXranvUvPVp=PvUp=P
100 99 imaeq2d PXranvUvPVp=PvUvp=vP
101 100 3anassrs PXranvUvPVp=PvUvp=vP
102 97 101 mpteq2da PXranvUvPVp=PvUvp=vUvP
103 102 rneqd PXranvUvPVp=PranvUvp=ranvUvP
104 simpl PXranvUvPVPX
105 simpr PXranvUvPVranvUvPV
106 3 103 104 105 fvmptd2 PXranvUvPVNP=ranvUvP
107 84 90 106 syl2anc UUnifOnXPXNP=ranvUvP
108 72 86 107 3eqtr2d UUnifOnXPXneiJP=ranvUvP