Theorem utopsnneiplem 23307

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 23292	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
3	1, 2	eqtrid 2790	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
4		simpll 763	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋))
5		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ∈ 𝒫 𝑋)
6	5	elpwid 4541	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ⊆ 𝑋)
7	6	sselda 3917	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝑋)
8		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋)
9		mptexg 7079	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
10		rnexg 7725	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
11	9, 10	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
12	11	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
13		utopsnneip.2	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
14	13	fvmpt2 6868	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
15	8, 12, 14	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
16	15	eleq2d 2824	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))))
17		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))
18	17	elrnmpt 5854	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ V → (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
19	18	elv 3428	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
20	16, 19	bitrdi 286	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
21	4, 7, 20	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
22		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎)
23		nfre1 3234	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})
24	22, 23	nfan 1903	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣(((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
25		simplr 765	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → 𝑣 ∈ 𝑈)
26		eqimss2 3974	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑣 “ {𝑝}) → (𝑣 “ {𝑝}) ⊆ 𝑎)
27	26	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → (𝑣 “ {𝑝}) ⊆ 𝑎)
28		imaeq1 5953	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑣 → (𝑤 “ {𝑝}) = (𝑣 “ {𝑝}))
29	28	sseq1d 3948	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑣 → ((𝑤 “ {𝑝}) ⊆ 𝑎 ↔ (𝑣 “ {𝑝}) ⊆ 𝑎))
30	29	rspcev 3552	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑣 “ {𝑝}) ⊆ 𝑎) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
31	25, 27, 30	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
32		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
33	24, 31, 32	r19.29af 3259	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
34	4	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋))
35	7	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑝 ∈ 𝑋)
36	34, 35	jca 511	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋))
37		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ⊆ 𝑎)
38	6	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ⊆ 𝑋)
39		simplr 765	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑤 ∈ 𝑈)
40		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝})
41		imaeq1 5953	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
42	41	rspceeqv 3567	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ 𝑈 ∧ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝})) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
43	40, 42	mpan2 687	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑈 → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
44	43	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
45		vex 3426	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑤 ∈ V
46	45	imaex 7737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 “ {𝑝}) ∈ V
47	13	ustuqtoplem 23299	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ V) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
48	46, 47	mpan2 687	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
49	48	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
50	44, 49	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))
51	34, 35, 39, 50	syl21anc 834	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))
52		sseq1 3942	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑎 ↔ (𝑤 “ {𝑝}) ⊆ 𝑎))
53	52	3anbi2d 1439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋)))
54		eleq1 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑝) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)))
55	53, 54	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))))
56	55	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))))
57	13	ustuqtop1 23301	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))
58	46, 56, 57	vtocl 3488	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))
59	36, 37, 38, 51, 58	syl31anc 1371	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ∈ (𝑁‘𝑝))
60	36, 20	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
61	59, 60	mpbid 231	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
62	61	r19.29an 3216	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
63	33, 62	impbida 797	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
64	21, 63	bitrd 278	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
65	64	ralbidva 3119	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝) ↔ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
66	65	rabbidva 3402	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
67	3, 66	eqtr4d 2781	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)})
68		utopsnneip.1	. . . . . 6 ⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}
69	67, 68	eqtr4di 2797	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = 𝐾)
70	69	fveq2d 6760	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (nei‘𝐽) = (nei‘𝐾))
71	70	fveq1d 6758	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃}))
72	71	adantr 480	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃}))
73	13	ustuqtop0 23300	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
74	13	ustuqtop1 23301	. . . . 5 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
75	13	ustuqtop2 23302	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
76	13	ustuqtop3 23303	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
77	13	ustuqtop4 23304	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
78	13	ustuqtop5 23305	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
79	68, 73, 74, 75, 76, 77, 78	neiptopnei 22191	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝})))
80	79	adantr 480	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝})))
81		simpr 484	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃)
82	81	sneqd 4570	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → {𝑝} = {𝑃})
83	82	fveq2d 6760	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → ((nei‘𝐾)‘{𝑝}) = ((nei‘𝐾)‘{𝑃}))
84		simpr 484	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑃 ∈ 𝑋)
85		fvexd 6771	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐾)‘{𝑃}) ∈ V)
86	80, 83, 84, 85	fvmptd 6864	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ((nei‘𝐾)‘{𝑃}))
87		mptexg 7079	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
88		rnexg 7725	. . . . 5 ⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
89	87, 88	syl 17	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
90	89	adantr 480	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
91		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑣 𝑃 ∈ 𝑋
92		nfmpt1 5178	. . . . . . . . . 10 ⊢ Ⅎ𝑣(𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))
93	92	nfrn 5850	. . . . . . . . 9 ⊢ Ⅎ𝑣ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))
94	93	nfel1 2922	. . . . . . . 8 ⊢ Ⅎ𝑣ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V
95	91, 94	nfan 1903	. . . . . . 7 ⊢ Ⅎ𝑣(𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
96		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑣 𝑝 = 𝑃
97	95, 96	nfan 1903	. . . . . 6 ⊢ Ⅎ𝑣((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃)
98		simpr2 1193	. . . . . . . . 9 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → 𝑝 = 𝑃)
99	98	sneqd 4570	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → {𝑝} = {𝑃})
100	99	imaeq2d 5958	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃}))
101	100	3anassrs 1358	. . . . . 6 ⊢ ((((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) ∧ 𝑣 ∈ 𝑈) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃}))
102	97, 101	mpteq2da 5168	. . . . 5 ⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
103	102	rneqd 5836	. . . 4 ⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
104		simpl 482	. . . 4 ⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → 𝑃 ∈ 𝑋)
105		simpr 484	. . . 4 ⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
106	13, 103, 104, 105	fvmptd2 6865	. . 3 ⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
107	84, 90, 106	syl2anc 583	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
108	72, 86, 107	3eqtr2d 2784	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ⊆ wss 3883  𝒫 cpw 4530  {csn 4558   ↦ cmpt 5153  ran crn 5581   “ cima 5583  ‘cfv 6418  neicnei 22156  UnifOncust 23259  unifTopcutop 23290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-om 7688  df-1o 8267  df-er 8456  df-en 8692  df-fin 8695  df-fi 9100  df-top 21951  df-nei 22157  df-ust 23260  df-utop 23291

This theorem is referenced by:  utopsnneip  23308