This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( 𝑈 ∈ ( 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 ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )