Theorem utopsnneiplem 24372

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

Hypotheses

Ref	Expression
utoptop.1	⊢ 𝐽 = (unifTop‘𝑈)
utopsnneip.1	⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}
utopsnneip.2	⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))

Assertion

Ref	Expression
utopsnneiplem	⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))

Distinct variable groups:   𝑝,𝑎,𝐾   𝑁,𝑎,𝑝   𝑣,𝑝,𝑃   𝑣,𝑎,𝑈,𝑝   𝑋,𝑎,𝑝,𝑣

Allowed substitution hints:   𝑃(𝑎)   𝐽(𝑣,𝑝,𝑎)   𝐾(𝑣)   𝑁(𝑣)

Proof of Theorem utopsnneiplem

Dummy variables 𝑏 𝑞 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		utoptop.1	. . . . . . . 8 ⊢ 𝐽 = (unifTop‘𝑈)
2		utopval 24357	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
3	1, 2	eqtrid 2816	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
4		simpll 778	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋))
5		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ∈ 𝒫 𝑋)
6	5	elpwid 4576	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ⊆ 𝑋)
7	6	sselda 3945	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝑋)
8		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋)
9		mptexg 7220	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
10		rnexg 7898	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
11	9, 10	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
12	11	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
13		utopsnneip.2	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
14	13	fvmpt2 7002	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
15	8, 12, 14	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
16	15	eleq2d 2855	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))))
17		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))
18	17	elrnmpt 5949	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ V → (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
19	18	elv 3468	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
20	16, 19	bitrdi 290	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
21	4, 7, 20	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
22		nfv 1941	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎)
23		nfre1 3296	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})
24	22, 23	nfan 1926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣(((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
25		simplr 780	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → 𝑣 ∈ 𝑈)
26		eqimss2 4004	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑣 “ {𝑝}) → (𝑣 “ {𝑝}) ⊆ 𝑎)
27	26	adantl 486	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → (𝑣 “ {𝑝}) ⊆ 𝑎)
28		imaeq1 6058	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑣 → (𝑤 “ {𝑝}) = (𝑣 “ {𝑝}))
29	28	sseq1d 3976	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑣 → ((𝑤 “ {𝑝}) ⊆ 𝑎 ↔ (𝑣 “ {𝑝}) ⊆ 𝑎))
30	29	rspcev 3590	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑣 “ {𝑝}) ⊆ 𝑎) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
31	25, 27, 30	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
32		simpr 489	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
33	24, 31, 32	r19.29af 3280	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
34	4	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋))
35	7	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑝 ∈ 𝑋)
36	34, 35	jca 520	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋))
37		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ⊆ 𝑎)
38	6	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ⊆ 𝑋)
39		simplr 780	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑤 ∈ 𝑈)
40		eqid 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝})
41		imaeq1 6058	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
42	41	rspceeqv 3613	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ 𝑈 ∧ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝})) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
43	40, 42	mpan2 703	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑈 → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
44	43	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
45		vex 3467	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑤 ∈ V
46	45	imaex 7910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 “ {𝑝}) ∈ V
47	13	ustuqtoplem 24364	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ V) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
48	46, 47	mpan2 703	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
49	48	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
50	44, 49	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))
51	34, 35, 39, 50	syl21anc 850	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))
52		sseq1 3970	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑎 ↔ (𝑤 “ {𝑝}) ⊆ 𝑎))
53	52	3anbi2d 1467	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋)))
54		eleq1 2857	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑝) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)))
55	53, 54	anbi12d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))))
56	55	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))))
57	13	ustuqtop1 24366	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))
58	46, 56, 57	vtocl 3534	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))
59	36, 37, 38, 51, 58	syl31anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ∈ (𝑁‘𝑝))
60	36, 20	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
61	59, 60	mpbid 235	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
62	61	r19.29an 3175	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
63	33, 62	impbida 812	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
64	21, 63	bitrd 282	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
65	64	ralbidva 3192	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝) ↔ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
66	65	rabbidva 3429	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
67	3, 66	eqtr4d 2807	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)})
68		utopsnneip.1	. . . . . 6 ⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}
69	67, 68	eqtr4di 2822	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = 𝐾)
70	69	fveq2d 6886	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (nei‘𝐽) = (nei‘𝐾))
71	70	fveq1d 6884	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃}))
72	71	adantr 485	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃}))
73	13	ustuqtop0 24365	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
74	13	ustuqtop1 24366	. . . . 5 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
75	13	ustuqtop2 24367	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
76	13	ustuqtop3 24368	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
77	13	ustuqtop4 24369	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
78	13	ustuqtop5 24370	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
79	68, 73, 74, 75, 76, 77, 78	neiptopnei 23257	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝})))
80	79	adantr 485	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝})))
81		simpr 489	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃)
82	81	sneqd 4606	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → {𝑝} = {𝑃})
83	82	fveq2d 6886	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → ((nei‘𝐾)‘{𝑝}) = ((nei‘𝐾)‘{𝑃}))
84		simpr 489	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑃 ∈ 𝑋)
85		fvexd 6897	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐾)‘{𝑃}) ∈ V)
86	80, 83, 84, 85	fvmptd 6998	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ((nei‘𝐾)‘{𝑃}))
87		mptexg 7220	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
88		rnexg 7898	. . . . 5 ⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
89	87, 88	syl 18	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
90	89	adantr 485	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
91		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑣 𝑃 ∈ 𝑋
92		nfmpt1 5214	. . . . . . . . . 10 ⊢ Ⅎ𝑣(𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))
93	92	nfrn 5943	. . . . . . . . 9 ⊢ Ⅎ𝑣ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))
94	93	nfel1 2947	. . . . . . . 8 ⊢ Ⅎ𝑣ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V
95	91, 94	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑣(𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
96		nfv 1941	. . . . . . 7 ⊢ Ⅎ𝑣 𝑝 = 𝑃
97	95, 96	nfan 1926	. . . . . 6 ⊢ Ⅎ𝑣((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃)
98		simpr2 1212	. . . . . . . . 9 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → 𝑝 = 𝑃)
99	98	sneqd 4606	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → {𝑝} = {𝑃})
100	99	imaeq2d 6063	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃}))
101	100	3anassrs 1379	. . . . . 6 ⊢ ((((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) ∧ 𝑣 ∈ 𝑈) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃}))
102	97, 101	mpteq2da 5207	. . . . 5 ⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
103	102	rneqd 5929	. . . 4 ⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
104		simpl 487	. . . 4 ⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → 𝑃 ∈ 𝑋)
105		simpr 489	. . . 4 ⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
106	13, 103, 104, 105	fvmptd2 6999	. . 3 ⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
107	84, 90, 106	syl2anc 595	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
108	72, 86, 107	3eqtr2d 2810	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  {crab 3423  Vcvv 3463   ⊆ wss 3913  𝒫 cpw 4567  {csn 4594   ↦ cmpt 5196  ran crn 5663   “ cima 5665  ‘cfv 6537  neicnei 23222  UnifOncust 24325  unifTopcutop 24355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-om 7862  df-1o 8452  df-2o 8453  df-en 8943  df-fin 8946  df-fi 9370  df-top 23019  df-nei 23223  df-ust 24326  df-utop 24356

This theorem is referenced by:  utopsnneip  24373