Theorem utopsnneiplem 24203

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 24188	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
3	1, 2	eqtrid 2784	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
4		simpll 767	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋))
5		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ∈ 𝒫 𝑋)
6	5	elpwid 4565	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ⊆ 𝑋)
7	6	sselda 3935	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝑋)
8		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋)
9		mptexg 7177	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V)
10		rnexg 7854	. . . . . . . . . . . . . . . 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 6961	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
15	8, 12, 14	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
16	15	eleq2d 2823	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))))
17		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))
18	17	elrnmpt 5915	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ V → (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
19	18	elv 3447	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
20	16, 19	bitrdi 287	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
21	4, 7, 20	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
22		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎)
23		nfre1 3263	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})
24	22, 23	nfan 1901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣(((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
25		simplr 769	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → 𝑣 ∈ 𝑈)
26		eqimss2 3995	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑣 “ {𝑝}) → (𝑣 “ {𝑝}) ⊆ 𝑎)
27	26	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → (𝑣 “ {𝑝}) ⊆ 𝑎)
28		imaeq1 6022	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑣 → (𝑤 “ {𝑝}) = (𝑣 “ {𝑝}))
29	28	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑣 → ((𝑤 “ {𝑝}) ⊆ 𝑎 ↔ (𝑣 “ {𝑝}) ⊆ 𝑎))
30	29	rspcev 3578	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑣 “ {𝑝}) ⊆ 𝑎) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
31	25, 27, 30	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
32		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
33	24, 31, 32	r19.29af 3247	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)
34	4	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋))
35	7	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑝 ∈ 𝑋)
36	34, 35	jca 511	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋))
37		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ⊆ 𝑎)
38	6	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ⊆ 𝑋)
39		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑤 ∈ 𝑈)
40		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝})
41		imaeq1 6022	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
42	41	rspceeqv 3601	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ 𝑈 ∧ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝})) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
43	40, 42	mpan2 692	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑈 → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
44	43	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
45		vex 3446	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑤 ∈ V
46	45	imaex 7866	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 “ {𝑝}) ∈ V
47	13	ustuqtoplem 24195	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ V) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
48	46, 47	mpan2 692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
49	48	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})))
50	44, 49	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))
51	34, 35, 39, 50	syl21anc 838	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))
52		sseq1 3961	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑎 ↔ (𝑤 “ {𝑝}) ⊆ 𝑎))
53	52	3anbi2d 1444	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋)))
54		eleq1 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑝) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)))
55	53, 54	anbi12d 633	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))))
56	55	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))))
57	13	ustuqtop1 24197	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))
58	46, 56, 57	vtocl 3517	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝))
59	36, 37, 38, 51, 58	syl31anc 1376	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ∈ (𝑁‘𝑝))
60	36, 20	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})))
61	59, 60	mpbid 232	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
62	61	r19.29an 3142	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))
63	33, 62	impbida 801	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
64	21, 63	bitrd 279	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
65	64	ralbidva 3159	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝) ↔ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎))
66	65	rabbidva 3407	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎})
67	3, 66	eqtr4d 2775	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)})
68		utopsnneip.1	. . . . . 6 ⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}
69	67, 68	eqtr4di 2790	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = 𝐾)
70	69	fveq2d 6846	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (nei‘𝐽) = (nei‘𝐾))
71	70	fveq1d 6844	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃}))
72	71	adantr 480	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃}))
73	13	ustuqtop0 24196	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
74	13	ustuqtop1 24197	. . . . 5 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
75	13	ustuqtop2 24198	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
76	13	ustuqtop3 24199	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
77	13	ustuqtop4 24200	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
78	13	ustuqtop5 24201	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
79	68, 73, 74, 75, 76, 77, 78	neiptopnei 23088	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝})))
80	79	adantr 480	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝})))
81		simpr 484	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃)
82	81	sneqd 4594	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → {𝑝} = {𝑃})
83	82	fveq2d 6846	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → ((nei‘𝐾)‘{𝑝}) = ((nei‘𝐾)‘{𝑃}))
84		simpr 484	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑃 ∈ 𝑋)
85		fvexd 6857	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐾)‘{𝑃}) ∈ V)
86	80, 83, 84, 85	fvmptd 6957	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ((nei‘𝐾)‘{𝑃}))
87		mptexg 7177	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
88		rnexg 7854	. . . . 5 ⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
89	87, 88	syl 17	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
90	89	adantr 480	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
91		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑣 𝑃 ∈ 𝑋
92		nfmpt1 5199	. . . . . . . . . 10 ⊢ Ⅎ𝑣(𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))
93	92	nfrn 5909	. . . . . . . . 9 ⊢ Ⅎ𝑣ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))
94	93	nfel1 2916	. . . . . . . 8 ⊢ Ⅎ𝑣ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V
95	91, 94	nfan 1901	. . . . . . 7 ⊢ Ⅎ𝑣(𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V)
96		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑣 𝑝 = 𝑃
97	95, 96	nfan 1901	. . . . . 6 ⊢ Ⅎ𝑣((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃)
98		simpr2 1197	. . . . . . . . 9 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → 𝑝 = 𝑃)
99	98	sneqd 4594	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → {𝑝} = {𝑃})
100	99	imaeq2d 6027	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃}))
101	100	3anassrs 1362	. . . . . 6 ⊢ ((((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) ∧ 𝑣 ∈ 𝑈) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃}))
102	97, 101	mpteq2da 5192	. . . . 5 ⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
103	102	rneqd 5895	. . . 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 6958	. . 3 ⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
107	84, 90, 106	syl2anc 585	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
108	72, 86, 107	3eqtr2d 2778	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ⊆ wss 3903  𝒫 cpw 4556  {csn 4582   ↦ cmpt 5181  ran crn 5633   “ cima 5635  ‘cfv 6500  neicnei 23053  UnifOncust 24156  unifTopcutop 24186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-om 7819  df-1o 8407  df-2o 8408  df-en 8896  df-fin 8899  df-fi 9326  df-top 22850  df-nei 23054  df-ust 24157  df-utop 24187

This theorem is referenced by:  utopsnneip  24204