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 = ( unifTop ` U )
utopsnneip.1 
|- K = { a e. ~P X | A. p e. a a e. ( N ` p ) }
utopsnneip.2 
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
Assertion utopsnneiplem 
|- ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( ( nei ` J ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )

Proof

Step Hyp Ref Expression
1 utoptop.1 
 |-  J = ( unifTop ` U )
2 utopsnneip.1 
 |-  K = { a e. ~P X | A. p e. a a e. ( N ` p ) }
3 utopsnneip.2 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
4 utopval 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = { a e. ~P X | A. p e. a E. w e. U ( w " { p } ) C_ a } )
5 1 4 eqtrid 
 |-  ( U e. ( UnifOn ` X ) -> J = { a e. ~P X | A. p e. a E. w e. U ( w " { p } ) C_ a } )
6 simpll 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) -> U e. ( UnifOn ` X ) )
7 simpr 
 |-  ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) -> a e. ~P X )
8 7 elpwid 
 |-  ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) -> a C_ X )
9 8 sselda 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) -> p e. X )
10 simpr 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> p e. X )
11 mptexg 
 |-  ( U e. ( UnifOn ` X ) -> ( v e. U |-> ( v " { p } ) ) e. _V )
12 rnexg 
 |-  ( ( v e. U |-> ( v " { p } ) ) e. _V -> ran ( v e. U |-> ( v " { p } ) ) e. _V )
13 11 12 syl 
 |-  ( U e. ( UnifOn ` X ) -> ran ( v e. U |-> ( v " { p } ) ) e. _V )
14 13 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ran ( v e. U |-> ( v " { p } ) ) e. _V )
15 3 fvmpt2 
 |-  ( ( p e. X /\ ran ( v e. U |-> ( v " { p } ) ) e. _V ) -> ( N ` p ) = ran ( v e. U |-> ( v " { p } ) ) )
16 10 14 15 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( N ` p ) = ran ( v e. U |-> ( v " { p } ) ) )
17 16 eleq2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> a e. ran ( v e. U |-> ( v " { p } ) ) ) )
18 eqid 
 |-  ( v e. U |-> ( v " { p } ) ) = ( v e. U |-> ( v " { p } ) )
19 18 elrnmpt 
 |-  ( a e. _V -> ( a e. ran ( v e. U |-> ( v " { p } ) ) <-> E. v e. U a = ( v " { p } ) ) )
20 19 elv 
 |-  ( a e. ran ( v e. U |-> ( v " { p } ) ) <-> E. v e. U a = ( v " { p } ) )
21 17 20 bitrdi 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. v e. U a = ( v " { p } ) ) )
22 6 9 21 syl2anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) -> ( a e. ( N ` p ) <-> E. v e. U a = ( v " { p } ) ) )
23 nfv 
 |-  F/ v ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a )
24 nfre1 
 |-  F/ v E. v e. U a = ( v " { p } )
25 23 24 nfan 
 |-  F/ v ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ E. v e. U a = ( v " { p } ) )
26 simplr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ E. v e. U a = ( v " { p } ) ) /\ v e. U ) /\ a = ( v " { p } ) ) -> v e. U )
27 eqimss2 
 |-  ( a = ( v " { p } ) -> ( v " { p } ) C_ a )
28 27 adantl 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ E. v e. U a = ( v " { p } ) ) /\ v e. U ) /\ a = ( v " { p } ) ) -> ( v " { p } ) C_ a )
29 imaeq1 
 |-  ( w = v -> ( w " { p } ) = ( v " { p } ) )
30 29 sseq1d 
 |-  ( w = v -> ( ( w " { p } ) C_ a <-> ( v " { p } ) C_ a ) )
31 30 rspcev 
 |-  ( ( v e. U /\ ( v " { p } ) C_ a ) -> E. w e. U ( w " { p } ) C_ a )
32 26 28 31 syl2anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ E. v e. U a = ( v " { p } ) ) /\ v e. U ) /\ a = ( v " { p } ) ) -> E. w e. U ( w " { p } ) C_ a )
33 simpr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ E. v e. U a = ( v " { p } ) ) -> E. v e. U a = ( v " { p } ) )
34 25 32 33 r19.29af 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ E. v e. U a = ( v " { p } ) ) -> E. w e. U ( w " { p } ) C_ a )
35 6 ad2antrr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> U e. ( UnifOn ` X ) )
36 9 ad2antrr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> p e. X )
37 35 36 jca 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> ( U e. ( UnifOn ` X ) /\ p e. X ) )
38 simpr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> ( w " { p } ) C_ a )
39 8 ad3antrrr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> a C_ X )
40 simplr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> w e. U )
41 eqid 
 |-  ( w " { p } ) = ( w " { p } )
42 imaeq1 
 |-  ( u = w -> ( u " { p } ) = ( w " { p } ) )
43 42 rspceeqv 
 |-  ( ( w e. U /\ ( w " { p } ) = ( w " { p } ) ) -> E. u e. U ( w " { p } ) = ( u " { p } ) )
44 41 43 mpan2 
 |-  ( w e. U -> E. u e. U ( w " { p } ) = ( u " { p } ) )
45 44 adantl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) -> E. u e. U ( w " { p } ) = ( u " { p } ) )
46 vex 
 |-  w e. _V
47 46 imaex 
 |-  ( w " { p } ) e. _V
48 3 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ ( w " { p } ) e. _V ) -> ( ( w " { p } ) e. ( N ` p ) <-> E. u e. U ( w " { p } ) = ( u " { p } ) ) )
49 47 48 mpan2 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( ( w " { p } ) e. ( N ` p ) <-> E. u e. U ( w " { p } ) = ( u " { p } ) ) )
50 49 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) -> ( ( w " { p } ) e. ( N ` p ) <-> E. u e. U ( w " { p } ) = ( u " { p } ) ) )
51 45 50 mpbird 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) -> ( w " { p } ) e. ( N ` p ) )
52 35 36 40 51 syl21anc 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> ( w " { p } ) e. ( N ` p ) )
53 sseq1 
 |-  ( b = ( w " { p } ) -> ( b C_ a <-> ( w " { p } ) C_ a ) )
54 53 3anbi2d 
 |-  ( b = ( w " { p } ) -> ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b C_ a /\ a C_ X ) <-> ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ ( w " { p } ) C_ a /\ a C_ X ) ) )
55 eleq1 
 |-  ( b = ( w " { p } ) -> ( b e. ( N ` p ) <-> ( w " { p } ) e. ( N ` p ) ) )
56 54 55 anbi12d 
 |-  ( b = ( w " { p } ) -> ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b C_ a /\ a C_ X ) /\ b e. ( N ` p ) ) <-> ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ ( w " { p } ) C_ a /\ a C_ X ) /\ ( w " { p } ) e. ( N ` p ) ) ) )
57 56 imbi1d 
 |-  ( b = ( w " { p } ) -> ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b C_ a /\ a C_ X ) /\ b e. ( N ` p ) ) -> a e. ( N ` p ) ) <-> ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ ( w " { p } ) C_ a /\ a C_ X ) /\ ( w " { p } ) e. ( N ` p ) ) -> a e. ( N ` p ) ) ) )
58 3 ustuqtop1 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b C_ a /\ a C_ X ) /\ b e. ( N ` p ) ) -> a e. ( N ` p ) )
59 47 57 58 vtocl 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ ( w " { p } ) C_ a /\ a C_ X ) /\ ( w " { p } ) e. ( N ` p ) ) -> a e. ( N ` p ) )
60 37 38 39 52 59 syl31anc 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> a e. ( N ` p ) )
61 37 21 syl 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> ( a e. ( N ` p ) <-> E. v e. U a = ( v " { p } ) ) )
62 60 61 mpbid 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ w e. U ) /\ ( w " { p } ) C_ a ) -> E. v e. U a = ( v " { p } ) )
63 62 r19.29an 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) /\ E. w e. U ( w " { p } ) C_ a ) -> E. v e. U a = ( v " { p } ) )
64 34 63 impbida 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) -> ( E. v e. U a = ( v " { p } ) <-> E. w e. U ( w " { p } ) C_ a ) )
65 22 64 bitrd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) /\ p e. a ) -> ( a e. ( N ` p ) <-> E. w e. U ( w " { p } ) C_ a ) )
66 65 ralbidva 
 |-  ( ( U e. ( UnifOn ` X ) /\ a e. ~P X ) -> ( A. p e. a a e. ( N ` p ) <-> A. p e. a E. w e. U ( w " { p } ) C_ a ) )
67 66 rabbidva 
 |-  ( U e. ( UnifOn ` X ) -> { a e. ~P X | A. p e. a a e. ( N ` p ) } = { a e. ~P X | A. p e. a E. w e. U ( w " { p } ) C_ a } )
68 5 67 eqtr4d 
 |-  ( U e. ( UnifOn ` X ) -> J = { a e. ~P X | A. p e. a a e. ( N ` p ) } )
69 68 2 eqtr4di 
 |-  ( U e. ( UnifOn ` X ) -> J = K )
70 69 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( nei ` J ) = ( nei ` K ) )
71 70 fveq1d 
 |-  ( U e. ( UnifOn ` X ) -> ( ( nei ` J ) ` { P } ) = ( ( nei ` K ) ` { P } ) )
72 71 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( ( nei ` J ) ` { P } ) = ( ( nei ` K ) ` { P } ) )
73 3 ustuqtop0 
 |-  ( U e. ( UnifOn ` X ) -> N : X --> ~P ~P X )
74 3 ustuqtop1 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
75 3 ustuqtop2 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
76 3 ustuqtop3 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
77 3 ustuqtop4 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
78 3 ustuqtop5 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> X e. ( N ` p ) )
79 2 73 74 75 76 77 78 neiptopnei 
 |-  ( U e. ( UnifOn ` X ) -> N = ( p e. X |-> ( ( nei ` K ) ` { p } ) ) )
80 79 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> N = ( p e. X |-> ( ( nei ` K ) ` { p } ) ) )
81 simpr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ p = P ) -> p = P )
82 81 sneqd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ p = P ) -> { p } = { P } )
83 82 fveq2d 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ P e. X ) /\ p = P ) -> ( ( nei ` K ) ` { p } ) = ( ( nei ` K ) ` { P } ) )
84 simpr 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> P e. X )
85 fvexd 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( ( nei ` K ) ` { P } ) e. _V )
86 80 83 84 85 fvmptd 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( N ` P ) = ( ( nei ` K ) ` { P } ) )
87 mptexg 
 |-  ( U e. ( UnifOn ` X ) -> ( v e. U |-> ( v " { P } ) ) e. _V )
88 rnexg 
 |-  ( ( v e. U |-> ( v " { P } ) ) e. _V -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
89 87 88 syl 
 |-  ( U e. ( UnifOn ` X ) -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
90 89 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
91 nfv 
 |-  F/ v P e. X
92 nfmpt1 
 |-  F/_ v ( v e. U |-> ( v " { P } ) )
93 92 nfrn 
 |-  F/_ v ran ( v e. U |-> ( v " { P } ) )
94 93 nfel1 
 |-  F/ v ran ( v e. U |-> ( v " { P } ) ) e. _V
95 91 94 nfan 
 |-  F/ v ( P e. X /\ ran ( v e. U |-> ( v " { P } ) ) e. _V )
96 nfv 
 |-  F/ v p = P
97 95 96 nfan 
 |-  F/ v ( ( P e. X /\ ran ( v e. U |-> ( v " { P } ) ) e. _V ) /\ p = P )
98 simpr2 
 |-  ( ( P e. X /\ ( ran ( v e. U |-> ( v " { P } ) ) e. _V /\ p = P /\ v e. U ) ) -> p = P )
99 98 sneqd 
 |-  ( ( P e. X /\ ( ran ( v e. U |-> ( v " { P } ) ) e. _V /\ p = P /\ v e. U ) ) -> { p } = { P } )
100 99 imaeq2d 
 |-  ( ( P e. X /\ ( ran ( v e. U |-> ( v " { P } ) ) e. _V /\ p = P /\ v e. U ) ) -> ( v " { p } ) = ( v " { P } ) )
101 100 3anassrs 
 |-  ( ( ( ( P e. X /\ ran ( v e. U |-> ( v " { P } ) ) e. _V ) /\ p = P ) /\ v e. U ) -> ( v " { p } ) = ( v " { P } ) )
102 97 101 mpteq2da 
 |-  ( ( ( P e. X /\ ran ( v e. U |-> ( v " { P } ) ) e. _V ) /\ p = P ) -> ( v e. U |-> ( v " { p } ) ) = ( v e. U |-> ( v " { P } ) ) )
103 102 rneqd 
 |-  ( ( ( P e. X /\ ran ( v e. U |-> ( v " { P } ) ) e. _V ) /\ p = P ) -> ran ( v e. U |-> ( v " { p } ) ) = ran ( v e. U |-> ( v " { P } ) ) )
104 simpl 
 |-  ( ( P e. X /\ ran ( v e. U |-> ( v " { P } ) ) e. _V ) -> P e. X )
105 simpr 
 |-  ( ( P e. X /\ ran ( v e. U |-> ( v " { P } ) ) e. _V ) -> ran ( v e. U |-> ( v " { P } ) ) e. _V )
106 3 103 104 105 fvmptd2 
 |-  ( ( P e. X /\ ran ( v e. U |-> ( v " { P } ) ) e. _V ) -> ( N ` P ) = ran ( v e. U |-> ( v " { P } ) ) )
107 84 90 106 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( N ` P ) = ran ( v e. U |-> ( v " { P } ) ) )
108 72 86 107 3eqtr2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( ( nei ` J ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )