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 𝐽 = ( unifTop ‘ 𝑈 )
utopsnneip.1 𝐾 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝𝑎 𝑎 ∈ ( 𝑁𝑝 ) }
utopsnneip.2 𝑁 = ( 𝑝𝑋 ↦ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
Assertion utopsnneiplem ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )

Proof

Step Hyp Ref Expression
1 utoptop.1 𝐽 = ( unifTop ‘ 𝑈 )
2 utopsnneip.1 𝐾 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝𝑎 𝑎 ∈ ( 𝑁𝑝 ) }
3 utopsnneip.2 𝑁 = ( 𝑝𝑋 ↦ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
4 utopval ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝𝑎𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 } )
5 1 4 syl5eq ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝𝑎𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 } )
6 simpll ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
7 simpr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑎 ∈ 𝒫 𝑋 )
8 7 elpwid ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑎𝑋 )
9 8 sselda ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) → 𝑝𝑋 )
10 simpr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → 𝑝𝑋 )
11 mptexg ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V )
12 rnexg ( ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V → ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V )
13 11 12 syl ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V )
14 13 adantr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V )
15 3 fvmpt2 ( ( 𝑝𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V ) → ( 𝑁𝑝 ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
16 10 14 15 syl2anc ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ( 𝑁𝑝 ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
17 16 eleq2d ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ( 𝑎 ∈ ( 𝑁𝑝 ) ↔ 𝑎 ∈ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ) )
18 eqid ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) )
19 18 elrnmpt ( 𝑎 ∈ V → ( 𝑎 ∈ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ↔ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) )
20 19 elv ( 𝑎 ∈ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ↔ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) )
21 17 20 bitrdi ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ( 𝑎 ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) )
22 6 9 21 syl2anc ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) → ( 𝑎 ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) )
23 nfv 𝑣 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 )
24 nfre1 𝑣𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } )
25 23 24 nfan 𝑣 ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) )
26 simplr ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑝 } ) ) → 𝑣𝑈 )
27 eqimss2 ( 𝑎 = ( 𝑣 “ { 𝑝 } ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑎 )
28 27 adantl ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑝 } ) ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑎 )
29 imaeq1 ( 𝑤 = 𝑣 → ( 𝑤 “ { 𝑝 } ) = ( 𝑣 “ { 𝑝 } ) )
30 29 sseq1d ( 𝑤 = 𝑣 → ( ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ↔ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑎 ) )
31 30 rspcev ( ( 𝑣𝑈 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑎 ) → ∃ 𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 )
32 26 28 31 syl2anc ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑝 } ) ) → ∃ 𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 )
33 simpr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) → ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) )
34 25 32 33 r19.29af ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) → ∃ 𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 )
35 6 ad2antrr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
36 9 ad2antrr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → 𝑝𝑋 )
37 35 36 jca ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) )
38 simpr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 )
39 8 ad3antrrr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → 𝑎𝑋 )
40 simplr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → 𝑤𝑈 )
41 eqid ( 𝑤 “ { 𝑝 } ) = ( 𝑤 “ { 𝑝 } )
42 imaeq1 ( 𝑢 = 𝑤 → ( 𝑢 “ { 𝑝 } ) = ( 𝑤 “ { 𝑝 } ) )
43 42 rspceeqv ( ( 𝑤𝑈 ∧ ( 𝑤 “ { 𝑝 } ) = ( 𝑤 “ { 𝑝 } ) ) → ∃ 𝑢𝑈 ( 𝑤 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } ) )
44 41 43 mpan2 ( 𝑤𝑈 → ∃ 𝑢𝑈 ( 𝑤 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } ) )
45 44 adantl ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) → ∃ 𝑢𝑈 ( 𝑤 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } ) )
46 vex 𝑤 ∈ V
47 46 imaex ( 𝑤 “ { 𝑝 } ) ∈ V
48 3 ustuqtoplem ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ ( 𝑤 “ { 𝑝 } ) ∈ V ) → ( ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑢𝑈 ( 𝑤 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } ) ) )
49 47 48 mpan2 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ( ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑢𝑈 ( 𝑤 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } ) ) )
50 49 adantr ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) → ( ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑢𝑈 ( 𝑤 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } ) ) )
51 45 50 mpbird ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) → ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) )
52 35 36 40 51 syl21anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) )
53 sseq1 ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( 𝑏𝑎 ↔ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) )
54 53 3anbi2d ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑏𝑎𝑎𝑋 ) ↔ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎𝑎𝑋 ) ) )
55 eleq1 ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( 𝑏 ∈ ( 𝑁𝑝 ) ↔ ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ) )
56 54 55 anbi12d ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑏𝑎𝑎𝑋 ) ∧ 𝑏 ∈ ( 𝑁𝑝 ) ) ↔ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎𝑎𝑋 ) ∧ ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ) ) )
57 56 imbi1d ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑏𝑎𝑎𝑋 ) ∧ 𝑏 ∈ ( 𝑁𝑝 ) ) → 𝑎 ∈ ( 𝑁𝑝 ) ) ↔ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎𝑎𝑋 ) ∧ ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ) → 𝑎 ∈ ( 𝑁𝑝 ) ) ) )
58 3 ustuqtop1 ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑏𝑎𝑎𝑋 ) ∧ 𝑏 ∈ ( 𝑁𝑝 ) ) → 𝑎 ∈ ( 𝑁𝑝 ) )
59 47 57 58 vtocl ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎𝑎𝑋 ) ∧ ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ) → 𝑎 ∈ ( 𝑁𝑝 ) )
60 37 38 39 52 59 syl31anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → 𝑎 ∈ ( 𝑁𝑝 ) )
61 37 21 syl ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → ( 𝑎 ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ) )
62 60 61 mpbid ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) )
63 62 r19.29an ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) ∧ ∃ 𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) → ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) )
64 34 63 impbida ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) → ( ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑝 } ) ↔ ∃ 𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) )
65 22 64 bitrd ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝𝑎 ) → ( 𝑎 ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) )
66 65 ralbidva ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑝𝑎 𝑎 ∈ ( 𝑁𝑝 ) ↔ ∀ 𝑝𝑎𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 ) )
67 66 rabbidva ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝𝑎 𝑎 ∈ ( 𝑁𝑝 ) } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝𝑎𝑤𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ 𝑎 } )
68 5 67 eqtr4d ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝𝑎 𝑎 ∈ ( 𝑁𝑝 ) } )
69 68 2 eqtr4di ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐽 = 𝐾 )
70 69 fveq2d ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( nei ‘ 𝐽 ) = ( nei ‘ 𝐾 ) )
71 70 fveq1d ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ( ( nei ‘ 𝐾 ) ‘ { 𝑃 } ) )
72 71 adantr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ( ( nei ‘ 𝐾 ) ‘ { 𝑃 } ) )
73 3 ustuqtop0 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
74 3 ustuqtop1 ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → 𝑏 ∈ ( 𝑁𝑝 ) )
75 3 ustuqtop2 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ( fi ‘ ( 𝑁𝑝 ) ) ⊆ ( 𝑁𝑝 ) )
76 3 ustuqtop3 ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → 𝑝𝑎 )
77 3 ustuqtop4 ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 𝑎 ∈ ( 𝑁𝑞 ) )
78 3 ustuqtop5 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → 𝑋 ∈ ( 𝑁𝑝 ) )
79 2 73 74 75 76 77 78 neiptopnei ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝐾 ) ‘ { 𝑝 } ) ) )
80 79 adantr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → 𝑁 = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝐾 ) ‘ { 𝑝 } ) ) )
81 simpr ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
82 81 sneqd ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑝 = 𝑃 ) → { 𝑝 } = { 𝑃 } )
83 82 fveq2d ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑝 = 𝑃 ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑝 } ) = ( ( nei ‘ 𝐾 ) ‘ { 𝑃 } ) )
84 simpr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → 𝑃𝑋 )
85 fvexd ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑃 } ) ∈ V )
86 80 83 84 85 fvmptd ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝑁𝑃 ) = ( ( nei ‘ 𝐾 ) ‘ { 𝑃 } ) )
87 mptexg ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
88 rnexg ( ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V → ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
89 87 88 syl ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
90 89 adantr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
91 nfv 𝑣 𝑃𝑋
92 nfmpt1 𝑣 ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) )
93 92 nfrn 𝑣 ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) )
94 93 nfel1 𝑣 ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V
95 91 94 nfan 𝑣 ( 𝑃𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
96 nfv 𝑣 𝑝 = 𝑃
97 95 96 nfan 𝑣 ( ( 𝑃𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) ∧ 𝑝 = 𝑃 )
98 simpr2 ( ( 𝑃𝑋 ∧ ( ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ∧ 𝑝 = 𝑃𝑣𝑈 ) ) → 𝑝 = 𝑃 )
99 98 sneqd ( ( 𝑃𝑋 ∧ ( ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ∧ 𝑝 = 𝑃𝑣𝑈 ) ) → { 𝑝 } = { 𝑃 } )
100 99 imaeq2d ( ( 𝑃𝑋 ∧ ( ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ∧ 𝑝 = 𝑃𝑣𝑈 ) ) → ( 𝑣 “ { 𝑝 } ) = ( 𝑣 “ { 𝑃 } ) )
101 100 3anassrs ( ( ( ( 𝑃𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) ∧ 𝑝 = 𝑃 ) ∧ 𝑣𝑈 ) → ( 𝑣 “ { 𝑝 } ) = ( 𝑣 “ { 𝑃 } ) )
102 97 101 mpteq2da ( ( ( 𝑃𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) ∧ 𝑝 = 𝑃 ) → ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
103 102 rneqd ( ( ( 𝑃𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) ∧ 𝑝 = 𝑃 ) → ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
104 simpl ( ( 𝑃𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) → 𝑃𝑋 )
105 simpr ( ( 𝑃𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) → ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
106 3 103 104 105 fvmptd2 ( ( 𝑃𝑋 ∧ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) → ( 𝑁𝑃 ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
107 84 90 106 syl2anc ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝑁𝑃 ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
108 72 86 107 3eqtr2d ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )