Theorem neiptopnei 22627

Description: Lemma for neiptopreu 22628. (Contributed by Thierry Arnoux, 7-Jan-2018.)

Hypotheses

Ref	Expression
neiptop.o	⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}
neiptop.0	⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
neiptop.1	⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
neiptop.2	⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
neiptop.3	⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
neiptop.4	⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
neiptop.5	⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))

Assertion

Ref	Expression
neiptopnei	⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))

Distinct variable groups:   𝑝,𝑎,𝑁   𝑋,𝑎,𝑏,𝑝   𝐽,𝑎,𝑝   𝑋,𝑝   𝜑,𝑝   𝑁,𝑏   𝑋,𝑏   𝜑,𝑎,𝑏,𝑞,𝑝   𝑁,𝑝,𝑞   𝑋,𝑞   𝜑,𝑞

Allowed substitution hints:   𝐽(𝑞,𝑏)

Proof of Theorem neiptopnei

Dummy variables 𝑐 𝑑 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neiptop.0	. . 3 ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
2	1	feqmptd 6957	. 2 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)))
3	1	ffvelcdmda 7083	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
4	3	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
5	4	elpwid 4610	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ⊆ 𝒫 𝑋)
6		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
7	5, 6	sseldd 3982	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ 𝒫 𝑋)
8	7	elpwid 4610	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ⊆ 𝑋)
9		neiptop.o	. . . . . . . . . . 11 ⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}
10		neiptop.1	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
11		neiptop.2	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
12		neiptop.3	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
13		neiptop.4	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
14		neiptop.5	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
15	9, 1, 10, 11, 12, 13, 14	neiptopuni 22625	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
16	15	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
17	16	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑋 = ∪ 𝐽)
18	8, 17	sseqtrd 4021	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ⊆ ∪ 𝐽)
19		ssrab2 4076	. . . . . . . . . 10 ⊢ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋
20	19	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)
21		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑟 → (𝑁‘𝑞) = (𝑁‘𝑟))
22	21	eleq2d 2819	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑟 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑟)))
23	22	elrab 3682	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)))
24		simp-5l 783	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝜑)
25		simpr1l 1230	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ ((𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)) ∧ 𝑏 ∈ (𝑁‘𝑟) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})) → 𝑟 ∈ 𝑋)
26	25	3anassrs 1360	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑟 ∈ 𝑋)
27		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
28		simplr 767	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ∈ (𝑁‘𝑟))
29		sseq1 4006	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
30	29	3anbi2d 1441	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
31		eleq1w 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ (𝑁‘𝑟) ↔ 𝑏 ∈ (𝑁‘𝑟)))
32	30, 31	anbi12d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟))))
33	32	imbi1d 341	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
34		simpl1l 1224	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝜑)
35	9, 1, 10, 11, 12, 13, 14	neiptoptop 22626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ Top)
36	35	uniexd 7728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
37	15, 36	eqeltrd 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ V)
38		rabexg 5330	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ V → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V)
39		sseq2 4007	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
40		sseq1 4006	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ⊆ 𝑋 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋))
41	39, 40	3anbi23d 1439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
42	41	anbi1d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
43		eleq1 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ∈ (𝑁‘𝑟) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
44	42, 43	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
45		eleq1w 2816	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑟 → (𝑝 ∈ 𝑋 ↔ 𝑟 ∈ 𝑋))
46	45	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑟 ∈ 𝑋)))
47	46	3anbi1d 1440	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
48		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → (𝑁‘𝑝) = (𝑁‘𝑟))
49	48	eleq2d 2819	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑟)))
50	47, 49	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
51	48	eleq2d 2819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑟)))
52	50, 51	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑟 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))))
53	52, 10	chvarvv 2002	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))
54	44, 53	vtoclg 3556	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
55	37, 38, 54	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
56	34, 55	mpcom 38	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
57	33, 56	chvarvv 2002	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
58	57	3an1rs 1359	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
59	19, 58	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
60	24, 26, 27, 28, 59	syl211anc 1376	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
61		simplll 773	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝜑)
62		simprl 769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑟 ∈ 𝑋)
63		simprr 771	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑐 ∈ (𝑁‘𝑟))
64	48	eleq2d 2819	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑟)))
65	46, 64	anbi12d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟))))
66		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑠 → (𝑁‘𝑞) = (𝑁‘𝑠))
67	66	eleq2d 2819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = 𝑠 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑠)))
68	67	cbvralvw 3234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
70	48, 69	rexeqbidv 3343	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
71	65, 70	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))))
72		eleq1w 2816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
73	72	anbi2d 629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
74		eleq1w 2816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑞)))
75	74	rexralbidv 3220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)))
76	73, 75	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))))
77	76, 13	chvarvv 2002	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))
78	71, 77	chvarvv 2002	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
79	1	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ∈ 𝒫 𝒫 𝑋)
80	79	elpwid 4610	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ⊆ 𝒫 𝑋)
81	80	sselda 3981	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ∈ 𝒫 𝑋)
82	81	elpwid 4610	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ⊆ 𝑋)
83	82	sselda 3981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → 𝑠 ∈ 𝑋)
84	83	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → 𝑠 ∈ 𝑋))
85	84	ancrd 552	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
86	85	ralimdva 3167	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → (∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
87	86	reximdva 3168	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
88	87	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
89	78, 88	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
90	67	elrab 3682	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
91	90	ralbii 3093	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
92	91	rexbii 3094	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
93	89, 92	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
94		dfss3 3969	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
95	94	biimpri 227	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
96	95	reximi 3084	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
97	93, 96	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
98	61, 62, 63, 97	syl21anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
99	60, 98	r19.29a 3162	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
100	23, 99	sylan2b 594	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ 𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
101	100	ralrimiva 3146	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
102	48	eleq2d 2819	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑟 → ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
103	102	cbvralvw 3234	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
104	101, 103	sylibr 233	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝))
105	9	neipeltop 22624	. . . . . . . . 9 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ↔ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝)))
106	20, 104, 105	sylanbrc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽)
107		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋)
108	107	anim1i 615	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
109		fveq2 6888	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → (𝑁‘𝑞) = (𝑁‘𝑝))
110	109	eleq2d 2819	. . . . . . . . . 10 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑝)))
111	110	elrab 3682	. . . . . . . . 9 ⊢ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
112	108, 111	sylibr 233	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
113		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑞((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))
114		nfrab1 3451	. . . . . . . . 9 ⊢ Ⅎ𝑞{𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}
115		nfcv 2903	. . . . . . . . 9 ⊢ Ⅎ𝑞𝑐
116		rabid 3452	. . . . . . . . . 10 ⊢ (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)))
117		simplll 773	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝜑)
118		simprl 769	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑋)
119		simprr 771	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑐 ∈ (𝑁‘𝑞))
120		eleq1w 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
121	120	anbi2d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑞 ∈ 𝑋)))
122		fveq2 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
123	122	eleq2d 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑞)))
124	121, 123	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞))))
125		elequ1 2113	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑐 ↔ 𝑞 ∈ 𝑐))
126	124, 125	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐) ↔ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)))
127		elequ2 2121	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 ∈ 𝑎 ↔ 𝑝 ∈ 𝑐))
128	73, 127	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)))
129	128, 12	chvarvv 2002	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)
130	126, 129	chvarvv 2002	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)
131	117, 118, 119, 130	syl21anc 836	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑐)
132	131	ex 413	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ((𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐))
133	116, 132	biimtrid 241	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑞 ∈ 𝑐))
134	113, 114, 115, 133	ssrd 3986	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)
135		eleq2 2822	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑝 ∈ 𝑑 ↔ 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
136		sseq1 4006	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑑 ⊆ 𝑐 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐))
137	135, 136	anbi12d 631	. . . . . . . . 9 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)))
138	137	rspcev 3612	. . . . . . . 8 ⊢ (({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
139	106, 112, 134, 138	syl12anc 835	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
140	18, 139	jca 512	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
141		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑑(𝜑 ∧ 𝑝 ∈ 𝑋)
142		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑑 𝑐 ⊆ ∪ 𝐽
143		nfre1 3282	. . . . . . . . 9 ⊢ Ⅎ𝑑∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)
144	142, 143	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑑(𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
145	141, 144	nfan 1902	. . . . . . 7 ⊢ Ⅎ𝑑((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
146		simplll 773	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
147		simpr 485	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ⊆ 𝑐)
148		simpr1l 1230	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ ((𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ 𝐽)
149	148	3anassrs 1360	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ ∪ 𝐽)
150	146, 16	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑋 = ∪ 𝐽)
151	149, 150	sseqtrrd 4022	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ 𝑋)
152		simplr 767	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ∈ (𝑁‘𝑝))
153		sseq1 4006	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑐))
154	153	3anbi2d 1441	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
155		eleq1w 2816	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑑 ∈ (𝑁‘𝑝)))
156	154, 155	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝))))
157	156	imbi1d 341	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
158		sseq2 4007	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ 𝑐))
159		sseq1 4006	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑋 ↔ 𝑐 ⊆ 𝑋))
160	158, 159	3anbi23d 1439	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
161	160	anbi1d 630	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
162		eleq1w 2816	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
163	161, 162	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
164	163, 10	chvarvv 2002	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
165	157, 164	chvarvv 2002	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
166	146, 147, 151, 152, 165	syl31anc 1373	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
167	9	neipeltop 22624	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ 𝐽 ↔ (𝑑 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝)))
168	167	simprbi 497	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ 𝐽 → ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝))
169	168	r19.21bi 3248	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) → 𝑑 ∈ (𝑁‘𝑝))
170	169	anim1i 615	. . . . . . . . . 10 ⊢ (((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) ∧ 𝑑 ⊆ 𝑐) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
171	170	anasss 467	. . . . . . . . 9 ⊢ ((𝑑 ∈ 𝐽 ∧ (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
172	171	reximi2 3079	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
173	172	ad2antll 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
174	145, 166, 173	r19.29af 3265	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → 𝑐 ∈ (𝑁‘𝑝))
175	140, 174	impbida 799	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
176	107, 16	eleqtrd 2835	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ ∪ 𝐽)
177		eqid 2732	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
178	177	isneip 22600	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑝 ∈ ∪ 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
179	35, 176, 178	syl2an2r 683	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
180	175, 179	bitr4d 281	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
181	180	eqrdv 2730	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ((nei‘𝐽)‘{𝑝}))
182	181	mpteq2dva 5247	. 2 ⊢ (𝜑 → (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)) = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
183	2, 182	eqtrd 2772	1 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070  {crab 3432  Vcvv 3474   ⊆ wss 3947  𝒫 cpw 4601  {csn 4627  ∪ cuni 4907   ↦ cmpt 5230  ⟶wf 6536  ‘cfv 6540  ficfi 9401  Topctop 22386  neicnei 22592

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-om 7852  df-1o 8462  df-en 8936  df-fin 8939  df-fi 9402  df-top 22387  df-nei 22593

This theorem is referenced by:  neiptopreu  22628  utopsnneiplem  23743