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 23172

Description: Lemma for neiptopreu 23173. (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 6931	. 2 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)))
3	1	ffvelcdmda 7061	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
4	3	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
5	4	elpwid 4563	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ⊆ 𝒫 𝑋)
6		simpr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
7	5, 6	sseldd 3937	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ 𝒫 𝑋)
8	7	elpwid 4563	. . . . . . . 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 23170	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
16	15	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
17	16	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑋 = ∪ 𝐽)
18	8, 17	sseqtrd 3972	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ⊆ ∪ 𝐽)
19		ssrab2 4033	. . . . . . . . . 10 ⊢ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋
20	19	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)
21		fveq2 6863	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑟 → (𝑁‘𝑞) = (𝑁‘𝑟))
22	21	eleq2d 2847	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑟 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑟)))
23	22	elrab 3650	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)))
24		simp-5l 794	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝜑)
25		simpr1l 1243	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ ((𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)) ∧ 𝑏 ∈ (𝑁‘𝑟) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})) → 𝑟 ∈ 𝑋)
26	25	3anassrs 1373	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑟 ∈ 𝑋)
27		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
28		simplr 778	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ∈ (𝑁‘𝑟))
29		sseq1 3961	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
30	29	3anbi2d 1461	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
31		eleq1w 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ (𝑁‘𝑟) ↔ 𝑏 ∈ (𝑁‘𝑟)))
32	30, 31	anbi12d 641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟))))
33	32	imbi1d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
34		simpl1l 1237	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝜑)
35	9, 1, 10, 11, 12, 13, 14	neiptoptop 23171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ Top)
36	35	uniexd 7721	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
37	15, 36	eqeltrd 2861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ V)
38		rabexg 5292	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ V → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V)
39		sseq2 3962	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
40		sseq1 3961	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ⊆ 𝑋 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋))
41	39, 40	3anbi23d 1459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
42	41	anbi1d 640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
43		eleq1 2849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ∈ (𝑁‘𝑟) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
44	42, 43	imbi12d 346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
45		eleq1w 2844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑟 → (𝑝 ∈ 𝑋 ↔ 𝑟 ∈ 𝑋))
46	45	anbi2d 639	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑟 ∈ 𝑋)))
47	46	3anbi1d 1460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
48		fveq2 6863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → (𝑁‘𝑝) = (𝑁‘𝑟))
49	48	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑟)))
50	47, 49	anbi12d 641	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
51	48	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑟)))
52	50, 51	imbi12d 346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑟 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))))
53	52, 10	chvarvv 2008	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))
54	44, 53	vtoclg 3521	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
55	37, 38, 54	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
56	34, 55	mpcom 38	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
57	33, 56	chvarvv 2008	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
58	57	3an1rs 1372	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
59	19, 58	mpan2 701	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
60	24, 26, 27, 28, 59	syl211anc 1394	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
61		simplll 784	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝜑)
62		simprl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑟 ∈ 𝑋)
63		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑐 ∈ (𝑁‘𝑟))
64	48	eleq2d 2847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑟)))
65	46, 64	anbi12d 641	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟))))
66		fveq2 6863	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑠 → (𝑁‘𝑞) = (𝑁‘𝑠))
67	66	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = 𝑠 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑠)))
68	67	cbvralvw 3239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
70	48, 69	rexeqbidv 3336	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
71	65, 70	imbi12d 346	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))))
72		eleq1w 2844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
73	72	anbi2d 639	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
74		eleq1w 2844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑞)))
75	74	rexralbidv 3227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)))
76	73, 75	imbi12d 346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))))
77	76, 13	chvarvv 2008	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))
78	71, 77	chvarvv 2008	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
79	1	ffvelcdmda 7061	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ∈ 𝒫 𝒫 𝑋)
80	79	elpwid 4563	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ⊆ 𝒫 𝑋)
81	80	sselda 3936	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ∈ 𝒫 𝑋)
82	81	elpwid 4563	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ⊆ 𝑋)
83	82	sselda 3936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → 𝑠 ∈ 𝑋)
84	83	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → 𝑠 ∈ 𝑋))
85	84	ancrd 559	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
86	85	ralimdva 3173	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → (∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
87	86	reximdva 3174	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
88	87	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
89	78, 88	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
90	67	elrab 3650	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
91	90	ralbii 3107	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
92	91	rexbii 3108	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
93	89, 92	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
94		dfss3 3925	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
95	94	biimpri 230	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
96	95	reximi 3099	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
97	93, 96	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
98	61, 62, 63, 97	syl21anc 848	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
99	60, 98	r19.29a 3169	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
100	23, 99	sylan2b 603	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ 𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
101	100	ralrimiva 3153	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
102	48	eleq2d 2847	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑟 → ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
103	102	cbvralvw 3239	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
104	101, 103	sylibr 236	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝))
105	9	neipeltop 23169	. . . . . . . . 9 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ↔ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝)))
106	20, 104, 105	sylanbrc 592	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽)
107		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋)
108	107	anim1i 624	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
109		fveq2 6863	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → (𝑁‘𝑞) = (𝑁‘𝑝))
110	109	eleq2d 2847	. . . . . . . . . 10 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑝)))
111	110	elrab 3650	. . . . . . . . 9 ⊢ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
112	108, 111	sylibr 236	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
113		nfv 1933	. . . . . . . . 9 ⊢ Ⅎ𝑞((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))
114		nfrab1 3433	. . . . . . . . 9 ⊢ Ⅎ𝑞{𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}
115		nfcv 2923	. . . . . . . . 9 ⊢ Ⅎ𝑞𝑐
116		rabid 3434	. . . . . . . . . 10 ⊢ (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)))
117		simplll 784	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝜑)
118		simprl 780	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑋)
119		simprr 782	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑐 ∈ (𝑁‘𝑞))
120		eleq1w 2844	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
121	120	anbi2d 639	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑞 ∈ 𝑋)))
122		fveq2 6863	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
123	122	eleq2d 2847	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑞)))
124	121, 123	anbi12d 641	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞))))
125		elequ1 2148	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑐 ↔ 𝑞 ∈ 𝑐))
126	124, 125	imbi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐) ↔ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)))
127		elequ2 2156	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 ∈ 𝑎 ↔ 𝑝 ∈ 𝑐))
128	73, 127	imbi12d 346	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)))
129	128, 12	chvarvv 2008	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)
130	126, 129	chvarvv 2008	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)
131	117, 118, 119, 130	syl21anc 848	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑐)
132	131	ex 416	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ((𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐))
133	116, 132	biimtrid 244	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑞 ∈ 𝑐))
134	113, 114, 115, 133	ssrd 3941	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)
135		eleq2 2850	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑝 ∈ 𝑑 ↔ 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
136		sseq1 3961	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑑 ⊆ 𝑐 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐))
137	135, 136	anbi12d 641	. . . . . . . . 9 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)))
138	137	rspcev 3581	. . . . . . . 8 ⊢ (({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
139	106, 112, 134, 138	syl12anc 847	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
140	18, 139	jca 519	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
141		nfv 1933	. . . . . . . 8 ⊢ Ⅎ𝑑(𝜑 ∧ 𝑝 ∈ 𝑋)
142		nfv 1933	. . . . . . . . 9 ⊢ Ⅎ𝑑 𝑐 ⊆ ∪ 𝐽
143		nfre1 3286	. . . . . . . . 9 ⊢ Ⅎ𝑑∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)
144	142, 143	nfan 1918	. . . . . . . 8 ⊢ Ⅎ𝑑(𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
145	141, 144	nfan 1918	. . . . . . 7 ⊢ Ⅎ𝑑((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
146		simplll 784	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
147		simpr 488	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ⊆ 𝑐)
148		simpr1l 1243	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ ((𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ 𝐽)
149	148	3anassrs 1373	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ ∪ 𝐽)
150	146, 16	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑋 = ∪ 𝐽)
151	149, 150	sseqtrrd 3973	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ 𝑋)
152		simplr 778	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ∈ (𝑁‘𝑝))
153		sseq1 3961	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑐))
154	153	3anbi2d 1461	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
155		eleq1w 2844	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑑 ∈ (𝑁‘𝑝)))
156	154, 155	anbi12d 641	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝))))
157	156	imbi1d 343	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
158		sseq2 3962	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ 𝑐))
159		sseq1 3961	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑋 ↔ 𝑐 ⊆ 𝑋))
160	158, 159	3anbi23d 1459	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
161	160	anbi1d 640	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
162		eleq1w 2844	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
163	161, 162	imbi12d 346	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
164	163, 10	chvarvv 2008	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
165	157, 164	chvarvv 2008	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
166	146, 147, 151, 152, 165	syl31anc 1391	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
167	9	neipeltop 23169	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ 𝐽 ↔ (𝑑 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝)))
168	167	simprbi 501	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ 𝐽 → ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝))
169	168	r19.21bi 3253	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) → 𝑑 ∈ (𝑁‘𝑝))
170	169	anim1i 624	. . . . . . . . . 10 ⊢ (((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) ∧ 𝑑 ⊆ 𝑐) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
171	170	anasss 470	. . . . . . . . 9 ⊢ ((𝑑 ∈ 𝐽 ∧ (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
172	171	reximi2 3094	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
173	172	ad2antll 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
174	145, 166, 173	r19.29af 3270	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → 𝑐 ∈ (𝑁‘𝑝))
175	140, 174	impbida 810	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
176	107, 16	eleqtrd 2863	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ ∪ 𝐽)
177		eqid 2761	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
178	177	isneip 23145	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑝 ∈ ∪ 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
179	35, 176, 178	syl2an2r 695	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
180	175, 179	bitr4d 284	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
181	180	eqrdv 2759	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ((nei‘𝐽)‘{𝑝}))
182	181	mpteq2dva 5192	. 2 ⊢ (𝜑 → (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)) = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
183	2, 182	eqtrd 2796	1 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ∀wral 3075 ∃wrex 3085 {crab 3413 Vcvv 3453 ⊆ wss 3904 𝒫 cpw 4554 {csn 4581 ∪ cuni 4864 ↦ cmpt 5180 ⟶wf 6513 ‘cfv 6517 ficfi 9353 Topctop 22933 neicnei 23137

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-om 7843 df-1o 8432 df-2o 8433 df-en 8924 df-fin 8927 df-fi 9354 df-top 22934 df-nei 23138

This theorem is referenced by: neiptopreu 23173 utopsnneiplem 24287

W3C validator