neiptopnei - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > neiptopnei		Structured version Visualization version GIF version

Theorem neiptopnei 21447

Description: Lemma for neiptopreu 21448. (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 6564	. 2 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)))
3	1	ffvelrnda 6678	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
4	3	adantr 473	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
5	4	elpwid 4435	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ⊆ 𝒫 𝑋)
6		simpr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
7	5, 6	sseldd 3861	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ 𝒫 𝑋)
8	7	elpwid 4435	. . . . . . . 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 21445	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
16	15	adantr 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
17	16	adantr 473	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑋 = ∪ 𝐽)
18	8, 17	sseqtrd 3899	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ⊆ ∪ 𝐽)
19		ssrab2 3948	. . . . . . . . . 10 ⊢ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋
20	19	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)
21		fveq2 6501	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑟 → (𝑁‘𝑞) = (𝑁‘𝑟))
22	21	eleq2d 2851	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑟 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑟)))
23	22	elrab 3595	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)))
24		simp-5l 772	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝜑)
25		simpr1l 1210	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ ((𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)) ∧ 𝑏 ∈ (𝑁‘𝑟) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})) → 𝑟 ∈ 𝑋)
26	25	3anassrs 1340	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑟 ∈ 𝑋)
27		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
28		simplr 756	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ∈ (𝑁‘𝑟))
29		sseq1 3884	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
30	29	3anbi2d 1420	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
31		eleq1w 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ (𝑁‘𝑟) ↔ 𝑏 ∈ (𝑁‘𝑟)))
32	30, 31	anbi12d 621	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟))))
33	32	imbi1d 334	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
34		simpl1l 1204	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝜑)
35	9, 1, 10, 11, 12, 13, 14	neiptoptop 21446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ Top)
36		uniexg 7287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
38	15, 37	eqeltrd 2866	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ V)
39		rabexg 5091	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ V → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V)
40		sseq2 3885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
41		sseq1 3884	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ⊆ 𝑋 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋))
42	40, 41	3anbi23d 1418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
43	42	anbi1d 620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
44		eleq1 2853	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ∈ (𝑁‘𝑟) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
45	43, 44	imbi12d 337	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
46		eleq1w 2848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑟 → (𝑝 ∈ 𝑋 ↔ 𝑟 ∈ 𝑋))
47	46	anbi2d 619	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑟 ∈ 𝑋)))
48	47	3anbi1d 1419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
49		fveq2 6501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → (𝑁‘𝑝) = (𝑁‘𝑟))
50	49	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑟)))
51	48, 50	anbi12d 621	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
52	49	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑟)))
53	51, 52	imbi12d 337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑟 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))))
54	53, 10	chvarv 2327	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))
55	45, 54	vtoclg 3486	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
56	38, 39, 55	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
57	34, 56	mpcom 38	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
58	33, 57	chvarv 2327	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
59	58	3an1rs 1339	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
60	19, 59	mpan2 678	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
61	24, 26, 27, 28, 60	syl211anc 1356	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
62		simplll 762	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝜑)
63		simprl 758	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑟 ∈ 𝑋)
64		simprr 760	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑐 ∈ (𝑁‘𝑟))
65	49	eleq2d 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑟)))
66	47, 65	anbi12d 621	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟))))
67		fveq2 6501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑠 → (𝑁‘𝑞) = (𝑁‘𝑠))
68	67	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = 𝑠 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑠)))
69	68	cbvralv 3383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
71	49, 70	rexeqbidv 3342	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
72	66, 71	imbi12d 337	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))))
73		eleq1w 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
74	73	anbi2d 619	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
75		eleq1w 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑞)))
76	75	rexralbidv 3246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)))
77	74, 76	imbi12d 337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))))
78	77, 13	chvarv 2327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))
79	72, 78	chvarv 2327	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
80	1	ffvelrnda 6678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ∈ 𝒫 𝒫 𝑋)
81	80	elpwid 4435	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ⊆ 𝒫 𝑋)
82	81	sselda 3860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ∈ 𝒫 𝑋)
83	82	elpwid 4435	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ⊆ 𝑋)
84	83	sselda 3860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → 𝑠 ∈ 𝑋)
85	84	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → 𝑠 ∈ 𝑋))
86	85	ancrd 544	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
87	86	ralimdva 3127	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → (∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
88	87	reximdva 3219	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
89	88	adantr 473	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
90	79, 89	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
91	68	elrab 3595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
92	91	ralbii 3115	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
93	92	rexbii 3194	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
94	90, 93	sylibr 226	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
95		dfss3 3849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
96	95	biimpri 220	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
97	96	reximi 3190	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
98	94, 97	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
99	62, 63, 64, 98	syl21anc 825	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
100	61, 99	r19.29a 3234	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
101	23, 100	sylan2b 584	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ 𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
102	101	ralrimiva 3132	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
103	49	eleq2d 2851	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑟 → ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
104	103	cbvralv 3383	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
105	102, 104	sylibr 226	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝))
106	9	neipeltop 21444	. . . . . . . . 9 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ↔ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝)))
107	20, 105, 106	sylanbrc 575	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽)
108		simpr 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋)
109	108	anim1i 605	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
110		fveq2 6501	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → (𝑁‘𝑞) = (𝑁‘𝑝))
111	110	eleq2d 2851	. . . . . . . . . 10 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑝)))
112	111	elrab 3595	. . . . . . . . 9 ⊢ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
113	109, 112	sylibr 226	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
114		nfv 1873	. . . . . . . . 9 ⊢ Ⅎ𝑞((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))
115		nfrab1 3324	. . . . . . . . 9 ⊢ Ⅎ𝑞{𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}
116		nfcv 2932	. . . . . . . . 9 ⊢ Ⅎ𝑞𝑐
117		rabid 3317	. . . . . . . . . 10 ⊢ (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)))
118		simplll 762	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝜑)
119		simprl 758	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑋)
120		simprr 760	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑐 ∈ (𝑁‘𝑞))
121		eleq1w 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
122	121	anbi2d 619	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑞 ∈ 𝑋)))
123		fveq2 6501	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
124	123	eleq2d 2851	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑞)))
125	122, 124	anbi12d 621	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞))))
126		elequ1 2057	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑐 ↔ 𝑞 ∈ 𝑐))
127	125, 126	imbi12d 337	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐) ↔ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)))
128		elequ2 2064	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 ∈ 𝑎 ↔ 𝑝 ∈ 𝑐))
129	74, 128	imbi12d 337	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)))
130	129, 12	chvarv 2327	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)
131	127, 130	chvarv 2327	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)
132	118, 119, 120, 131	syl21anc 825	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑐)
133	132	ex 405	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ((𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐))
134	117, 133	syl5bi 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑞 ∈ 𝑐))
135	114, 115, 116, 134	ssrd 3865	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)
136		eleq2 2854	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑝 ∈ 𝑑 ↔ 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
137		sseq1 3884	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑑 ⊆ 𝑐 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐))
138	136, 137	anbi12d 621	. . . . . . . . 9 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)))
139	138	rspcev 3535	. . . . . . . 8 ⊢ (({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
140	107, 113, 135, 139	syl12anc 824	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
141	18, 140	jca 504	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
142		nfv 1873	. . . . . . . 8 ⊢ Ⅎ𝑑(𝜑 ∧ 𝑝 ∈ 𝑋)
143		nfv 1873	. . . . . . . . 9 ⊢ Ⅎ𝑑 𝑐 ⊆ ∪ 𝐽
144		nfre1 3251	. . . . . . . . 9 ⊢ Ⅎ𝑑∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)
145	143, 144	nfan 1862	. . . . . . . 8 ⊢ Ⅎ𝑑(𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
146	142, 145	nfan 1862	. . . . . . 7 ⊢ Ⅎ𝑑((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
147		simplll 762	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
148		simpr 477	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ⊆ 𝑐)
149		simpr1l 1210	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ ((𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ 𝐽)
150	149	3anassrs 1340	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ ∪ 𝐽)
151	147, 16	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑋 = ∪ 𝐽)
152	150, 151	sseqtr4d 3900	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ 𝑋)
153		simplr 756	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ∈ (𝑁‘𝑝))
154		sseq1 3884	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑐))
155	154	3anbi2d 1420	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
156		eleq1w 2848	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑑 ∈ (𝑁‘𝑝)))
157	155, 156	anbi12d 621	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝))))
158	157	imbi1d 334	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
159		sseq2 3885	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ 𝑐))
160		sseq1 3884	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑋 ↔ 𝑐 ⊆ 𝑋))
161	159, 160	3anbi23d 1418	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
162	161	anbi1d 620	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
163		eleq1w 2848	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
164	162, 163	imbi12d 337	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
165	164, 10	chvarv 2327	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
166	158, 165	chvarv 2327	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
167	147, 148, 152, 153, 166	syl31anc 1353	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
168	9	neipeltop 21444	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ 𝐽 ↔ (𝑑 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝)))
169	168	simprbi 489	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ 𝐽 → ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝))
170	169	r19.21bi 3158	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) → 𝑑 ∈ (𝑁‘𝑝))
171	170	anim1i 605	. . . . . . . . . 10 ⊢ (((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) ∧ 𝑑 ⊆ 𝑐) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
172	171	anasss 459	. . . . . . . . 9 ⊢ ((𝑑 ∈ 𝐽 ∧ (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
173	172	reximi2 3191	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
174	173	ad2antll 716	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
175	146, 167, 174	r19.29af 3272	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → 𝑐 ∈ (𝑁‘𝑝))
176	141, 175	impbida 788	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
177	108, 16	eleqtrd 2868	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ ∪ 𝐽)
178		eqid 2778	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
179	178	isneip 21420	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑝 ∈ ∪ 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
180	35, 177, 179	syl2an2r 672	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
181	176, 180	bitr4d 274	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
182	181	eqrdv 2776	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ((nei‘𝐽)‘{𝑝}))
183	182	mpteq2dva 5023	. 2 ⊢ (𝜑 → (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)) = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
184	2, 183	eqtrd 2814	1 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ∀wral 3088 ∃wrex 3089 {crab 3092 Vcvv 3415 ⊆ wss 3831 𝒫 cpw 4423 {csn 4442 ∪ cuni 4713 ↦ cmpt 5009 ⟶wf 6186 ‘cfv 6190 ficfi 8671 Topctop 21208 neicnei 21412

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5050 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-reu 3095 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-tp 4447 df-op 4449 df-uni 4714 df-int 4751 df-iun 4795 df-br 4931 df-opab 4993 df-mpt 5010 df-tr 5032 df-id 5313 df-eprel 5318 df-po 5327 df-so 5328 df-fr 5367 df-we 5369 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-pred 5988 df-ord 6034 df-on 6035 df-lim 6036 df-suc 6037 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-ov 6981 df-oprab 6982 df-mpo 6983 df-om 7399 df-wrecs 7752 df-recs 7814 df-rdg 7852 df-1o 7907 df-oadd 7911 df-er 8091 df-en 8309 df-fin 8312 df-fi 8672 df-top 21209 df-nei 21413

This theorem is referenced by: neiptopreu 21448 utopsnneiplem 22562

W3C validator