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 21742

Description: Lemma for neiptopreu 21743. (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 6735	. 2 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)))
3	1	ffvelrnda 6853	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
4	3	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
5	4	elpwid 4552	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ⊆ 𝒫 𝑋)
6		simpr 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
7	5, 6	sseldd 3970	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ 𝒫 𝑋)
8	7	elpwid 4552	. . . . . . . 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 21740	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
16	15	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
17	16	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑋 = ∪ 𝐽)
18	8, 17	sseqtrd 4009	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ⊆ ∪ 𝐽)
19		ssrab2 4058	. . . . . . . . . 10 ⊢ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋
20	19	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)
21		fveq2 6672	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑟 → (𝑁‘𝑞) = (𝑁‘𝑟))
22	21	eleq2d 2900	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑟 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑟)))
23	22	elrab 3682	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)))
24		simp-5l 783	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝜑)
25		simpr1l 1226	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ ((𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)) ∧ 𝑏 ∈ (𝑁‘𝑟) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})) → 𝑟 ∈ 𝑋)
26	25	3anassrs 1356	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑟 ∈ 𝑋)
27		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
28		simplr 767	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ∈ (𝑁‘𝑟))
29		sseq1 3994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
30	29	3anbi2d 1437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
31		eleq1w 2897	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ (𝑁‘𝑟) ↔ 𝑏 ∈ (𝑁‘𝑟)))
32	30, 31	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟))))
33	32	imbi1d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
34		simpl1l 1220	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝜑)
35	9, 1, 10, 11, 12, 13, 14	neiptoptop 21741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ Top)
36	35	uniexd 7470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
37	15, 36	eqeltrd 2915	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ V)
38		rabexg 5236	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ V → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V)
39		sseq2 3995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
40		sseq1 3994	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ⊆ 𝑋 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋))
41	39, 40	3anbi23d 1435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
42	41	anbi1d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
43		eleq1 2902	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ∈ (𝑁‘𝑟) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
44	42, 43	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
45		eleq1w 2897	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑟 → (𝑝 ∈ 𝑋 ↔ 𝑟 ∈ 𝑋))
46	45	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑟 ∈ 𝑋)))
47	46	3anbi1d 1436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
48		fveq2 6672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → (𝑁‘𝑝) = (𝑁‘𝑟))
49	48	eleq2d 2900	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑟)))
50	47, 49	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
51	48	eleq2d 2900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑟)))
52	50, 51	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑟 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))))
53	52, 10	chvarvv 2005	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))
54	44, 53	vtoclg 3569	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
55	37, 38, 54	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
56	34, 55	mpcom 38	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
57	33, 56	chvarvv 2005	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
58	57	3an1rs 1355	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
59	19, 58	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
60	24, 26, 27, 28, 59	syl211anc 1372	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
61		simplll 773	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝜑)
62		simprl 769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑟 ∈ 𝑋)
63		simprr 771	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑐 ∈ (𝑁‘𝑟))
64	48	eleq2d 2900	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑟)))
65	46, 64	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟))))
66		fveq2 6672	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑠 → (𝑁‘𝑞) = (𝑁‘𝑠))
67	66	eleq2d 2900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = 𝑠 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑠)))
68	67	cbvralvw 3451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
70	48, 69	rexeqbidv 3404	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
71	65, 70	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))))
72		eleq1w 2897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
73	72	anbi2d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
74		eleq1w 2897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑞)))
75	74	rexralbidv 3303	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)))
76	73, 75	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))))
77	76, 13	chvarvv 2005	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))
78	71, 77	chvarvv 2005	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
79	1	ffvelrnda 6853	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ∈ 𝒫 𝒫 𝑋)
80	79	elpwid 4552	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ⊆ 𝒫 𝑋)
81	80	sselda 3969	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ∈ 𝒫 𝑋)
82	81	elpwid 4552	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ⊆ 𝑋)
83	82	sselda 3969	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → 𝑠 ∈ 𝑋)
84	83	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → 𝑠 ∈ 𝑋))
85	84	ancrd 554	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
86	85	ralimdva 3179	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → (∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
87	86	reximdva 3276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
88	87	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
89	78, 88	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
90	67	elrab 3682	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
91	90	ralbii 3167	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
92	91	rexbii 3249	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
93	89, 92	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
94		dfss3 3958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
95	94	biimpri 230	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
96	95	reximi 3245	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
97	93, 96	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
98	61, 62, 63, 97	syl21anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
99	60, 98	r19.29a 3291	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
100	23, 99	sylan2b 595	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ 𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
101	100	ralrimiva 3184	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
102	48	eleq2d 2900	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑟 → ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
103	102	cbvralvw 3451	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
104	101, 103	sylibr 236	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝))
105	9	neipeltop 21739	. . . . . . . . 9 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ↔ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝)))
106	20, 104, 105	sylanbrc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽)
107		simpr 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋)
108	107	anim1i 616	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
109		fveq2 6672	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → (𝑁‘𝑞) = (𝑁‘𝑝))
110	109	eleq2d 2900	. . . . . . . . . 10 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑝)))
111	110	elrab 3682	. . . . . . . . 9 ⊢ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
112	108, 111	sylibr 236	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
113		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑞((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))
114		nfrab1 3386	. . . . . . . . 9 ⊢ Ⅎ𝑞{𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}
115		nfcv 2979	. . . . . . . . 9 ⊢ Ⅎ𝑞𝑐
116		rabid 3380	. . . . . . . . . 10 ⊢ (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)))
117		simplll 773	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝜑)
118		simprl 769	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑋)
119		simprr 771	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑐 ∈ (𝑁‘𝑞))
120		eleq1w 2897	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
121	120	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑞 ∈ 𝑋)))
122		fveq2 6672	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
123	122	eleq2d 2900	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑞)))
124	121, 123	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞))))
125		elequ1 2121	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑐 ↔ 𝑞 ∈ 𝑐))
126	124, 125	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐) ↔ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)))
127		elequ2 2129	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 ∈ 𝑎 ↔ 𝑝 ∈ 𝑐))
128	73, 127	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)))
129	128, 12	chvarvv 2005	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)
130	126, 129	chvarvv 2005	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)
131	117, 118, 119, 130	syl21anc 835	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑐)
132	131	ex 415	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ((𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐))
133	116, 132	syl5bi 244	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑞 ∈ 𝑐))
134	113, 114, 115, 133	ssrd 3974	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)
135		eleq2 2903	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑝 ∈ 𝑑 ↔ 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
136		sseq1 3994	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑑 ⊆ 𝑐 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐))
137	135, 136	anbi12d 632	. . . . . . . . 9 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)))
138	137	rspcev 3625	. . . . . . . 8 ⊢ (({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
139	106, 112, 134, 138	syl12anc 834	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
140	18, 139	jca 514	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
141		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑑(𝜑 ∧ 𝑝 ∈ 𝑋)
142		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑑 𝑐 ⊆ ∪ 𝐽
143		nfre1 3308	. . . . . . . . 9 ⊢ Ⅎ𝑑∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)
144	142, 143	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑑(𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
145	141, 144	nfan 1900	. . . . . . 7 ⊢ Ⅎ𝑑((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
146		simplll 773	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
147		simpr 487	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ⊆ 𝑐)
148		simpr1l 1226	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ ((𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ 𝐽)
149	148	3anassrs 1356	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ ∪ 𝐽)
150	146, 16	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑋 = ∪ 𝐽)
151	149, 150	sseqtrrd 4010	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ 𝑋)
152		simplr 767	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ∈ (𝑁‘𝑝))
153		sseq1 3994	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑐))
154	153	3anbi2d 1437	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
155		eleq1w 2897	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑑 ∈ (𝑁‘𝑝)))
156	154, 155	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝))))
157	156	imbi1d 344	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
158		sseq2 3995	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ 𝑐))
159		sseq1 3994	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑋 ↔ 𝑐 ⊆ 𝑋))
160	158, 159	3anbi23d 1435	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
161	160	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
162		eleq1w 2897	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
163	161, 162	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
164	163, 10	chvarvv 2005	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
165	157, 164	chvarvv 2005	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
166	146, 147, 151, 152, 165	syl31anc 1369	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
167	9	neipeltop 21739	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ 𝐽 ↔ (𝑑 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝)))
168	167	simprbi 499	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ 𝐽 → ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝))
169	168	r19.21bi 3210	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) → 𝑑 ∈ (𝑁‘𝑝))
170	169	anim1i 616	. . . . . . . . . 10 ⊢ (((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) ∧ 𝑑 ⊆ 𝑐) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
171	170	anasss 469	. . . . . . . . 9 ⊢ ((𝑑 ∈ 𝐽 ∧ (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
172	171	reximi2 3246	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
173	172	ad2antll 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
174	145, 166, 173	r19.29af 3333	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → 𝑐 ∈ (𝑁‘𝑝))
175	140, 174	impbida 799	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
176	107, 16	eleqtrd 2917	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ ∪ 𝐽)
177		eqid 2823	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
178	177	isneip 21715	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑝 ∈ ∪ 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
179	35, 176, 178	syl2an2r 683	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
180	175, 179	bitr4d 284	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
181	180	eqrdv 2821	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ((nei‘𝐽)‘{𝑝}))
182	181	mpteq2dva 5163	. 2 ⊢ (𝜑 → (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)) = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
183	2, 182	eqtrd 2858	1 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ∀wral 3140 ∃wrex 3141 {crab 3144 Vcvv 3496 ⊆ wss 3938 𝒫 cpw 4541 {csn 4569 ∪ cuni 4840 ↦ cmpt 5148 ⟶wf 6353 ‘cfv 6357 ficfi 8876 Topctop 21503 neicnei 21707

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-ral 3145 df-rex 3146 df-reu 3147 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-oadd 8108 df-er 8291 df-en 8512 df-fin 8515 df-fi 8877 df-top 21504 df-nei 21708

This theorem is referenced by: neiptopreu 21743 utopsnneiplem 22858

W3C validator