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 23140

Description: Lemma for neiptopreu 23141. (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 6977	. 2 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)))
3	1	ffvelcdmda 7104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
4	3	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ∈ 𝒫 𝒫 𝑋)
5	4	elpwid 4609	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑁‘𝑝) ⊆ 𝒫 𝑋)
6		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
7	5, 6	sseldd 3984	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ∈ 𝒫 𝑋)
8	7	elpwid 4609	. . . . . . . 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 23138	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
16	15	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
17	16	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑋 = ∪ 𝐽)
18	8, 17	sseqtrd 4020	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑐 ⊆ ∪ 𝐽)
19		ssrab2 4080	. . . . . . . . . 10 ⊢ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋
20	19	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)
21		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑟 → (𝑁‘𝑞) = (𝑁‘𝑟))
22	21	eleq2d 2827	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑟 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑟)))
23	22	elrab 3692	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)))
24		simp-5l 785	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝜑)
25		simpr1l 1231	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ ((𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟)) ∧ 𝑏 ∈ (𝑁‘𝑟) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})) → 𝑟 ∈ 𝑋)
26	25	3anassrs 1361	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑟 ∈ 𝑋)
27		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
28		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → 𝑏 ∈ (𝑁‘𝑟))
29		sseq1 4009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
30	29	3anbi2d 1443	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
31		eleq1w 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ (𝑁‘𝑟) ↔ 𝑏 ∈ (𝑁‘𝑟)))
32	30, 31	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟))))
33	32	imbi1d 341	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
34		simpl1l 1225	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝜑)
35	9, 1, 10, 11, 12, 13, 14	neiptoptop 23139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ Top)
36	35	uniexd 7762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
37	15, 36	eqeltrd 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ V)
38		rabexg 5337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ V → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V)
39		sseq2 4010	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
40		sseq1 4009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ⊆ 𝑋 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋))
41	39, 40	3anbi23d 1441	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋)))
42	41	anbi1d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
43		eleq1 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑏 ∈ (𝑁‘𝑟) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
44	42, 43	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))))
45		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = 𝑟 → (𝑝 ∈ 𝑋 ↔ 𝑟 ∈ 𝑋))
46	45	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑟 ∈ 𝑋)))
47	46	3anbi1d 1442	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
48		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑟 → (𝑁‘𝑝) = (𝑁‘𝑟))
49	48	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑟 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑟)))
50	47, 49	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟))))
51	48	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = 𝑟 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑟)))
52	50, 51	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑟 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))))
53	52, 10	chvarvv 1998	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → 𝑏 ∈ (𝑁‘𝑟))
54	44, 53	vtoclg 3554	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ V → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
55	37, 38, 54	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
56	34, 55	mpcom 38	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑎 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
57	33, 56	chvarvv 1998	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
58	57	3an1rs 1360	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
59	19, 58	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ 𝑏 ∈ (𝑁‘𝑟)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
60	24, 26, 27, 28, 59	syl211anc 1378	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
61		simplll 775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝜑)
62		simprl 771	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑟 ∈ 𝑋)
63		simprr 773	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → 𝑐 ∈ (𝑁‘𝑟))
64	48	eleq2d 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑟)))
65	46, 64	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟))))
66		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑠 → (𝑁‘𝑞) = (𝑁‘𝑠))
67	66	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 = 𝑠 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑠)))
68	67	cbvralvw 3237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑟 → (∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
70	48, 69	rexeqbidv 3347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠)))
71	65, 70	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))))
72		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
73	72	anbi2d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
74		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑞)))
75	74	rexralbidv 3223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞)))
76	73, 75	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))))
77	76, 13	chvarvv 1998	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑞))
78	71, 77	chvarvv 1998	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠))
79	1	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ∈ 𝒫 𝒫 𝑋)
80	79	elpwid 4609	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (𝑁‘𝑟) ⊆ 𝒫 𝑋)
81	80	sselda 3983	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ∈ 𝒫 𝑋)
82	81	elpwid 4609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → 𝑏 ⊆ 𝑋)
83	82	sselda 3983	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → 𝑠 ∈ 𝑋)
84	83	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → 𝑠 ∈ 𝑋))
85	84	ancrd 551	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) ∧ 𝑠 ∈ 𝑏) → (𝑐 ∈ (𝑁‘𝑠) → (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
86	85	ralimdva 3167	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑟)) → (∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
87	86	reximdva 3168	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑋) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
88	87	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑐 ∈ (𝑁‘𝑠) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠))))
89	78, 88	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
90	67	elrab 3692	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
91	90	ralbii 3093	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
92	91	rexbii 3094	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 (𝑠 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑠)))
93	89, 92	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
94		dfss3 3972	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ ∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
95	94	biimpri 228	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
96	95	reximi 3084	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 ∈ (𝑁‘𝑟)∀𝑠 ∈ 𝑏 𝑠 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
97	93, 96	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑟)) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
98	61, 62, 63, 97	syl21anc 838	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → ∃𝑏 ∈ (𝑁‘𝑟)𝑏 ⊆ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
99	60, 98	r19.29a 3162	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑟))) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
100	23, 99	sylan2b 594	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ 𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
101	100	ralrimiva 3146	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
102	48	eleq2d 2827	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑟 → ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟)))
103	102	cbvralvw 3237	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝) ↔ ∀𝑟 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑟))
104	101, 103	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝))
105	9	neipeltop 23137	. . . . . . . . 9 ⊢ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ↔ ({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ (𝑁‘𝑝)))
106	20, 104, 105	sylanbrc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽)
107		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋)
108	107	anim1i 615	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
109		fveq2 6906	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → (𝑁‘𝑞) = (𝑁‘𝑝))
110	109	eleq2d 2827	. . . . . . . . . 10 ⊢ (𝑞 = 𝑝 → (𝑐 ∈ (𝑁‘𝑞) ↔ 𝑐 ∈ (𝑁‘𝑝)))
111	110	elrab 3692	. . . . . . . . 9 ⊢ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑝 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑝)))
112	108, 111	sylibr 234	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)})
113		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑞((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))
114		nfrab1 3457	. . . . . . . . 9 ⊢ Ⅎ𝑞{𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}
115		nfcv 2905	. . . . . . . . 9 ⊢ Ⅎ𝑞𝑐
116		rabid 3458	. . . . . . . . . 10 ⊢ (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ↔ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)))
117		simplll 775	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝜑)
118		simprl 771	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑋)
119		simprr 773	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑐 ∈ (𝑁‘𝑞))
120		eleq1w 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
121	120	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → ((𝜑 ∧ 𝑝 ∈ 𝑋) ↔ (𝜑 ∧ 𝑞 ∈ 𝑋)))
122		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
123	122	eleq2d 2827	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑞)))
124	121, 123	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ↔ ((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞))))
125		elequ1 2115	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑐 ↔ 𝑞 ∈ 𝑐))
126	124, 125	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐) ↔ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)))
127		elequ2 2123	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 ∈ 𝑎 ↔ 𝑝 ∈ 𝑐))
128	73, 127	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)))
129	128, 12	chvarvv 1998	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑐)
130	126, 129	chvarvv 1998	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐)
131	117, 118, 119, 130	syl21anc 838	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) ∧ (𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞))) → 𝑞 ∈ 𝑐)
132	131	ex 412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ((𝑞 ∈ 𝑋 ∧ 𝑐 ∈ (𝑁‘𝑞)) → 𝑞 ∈ 𝑐))
133	116, 132	biimtrid 242	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑞 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → 𝑞 ∈ 𝑐))
134	113, 114, 115, 133	ssrd 3988	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)
135		eleq2 2830	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑝 ∈ 𝑑 ↔ 𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)}))
136		sseq1 4009	. . . . . . . . . 10 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → (𝑑 ⊆ 𝑐 ↔ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐))
137	135, 136	anbi12d 632	. . . . . . . . 9 ⊢ (𝑑 = {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} → ((𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)))
138	137	rspcev 3622	. . . . . . . 8 ⊢ (({𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ∧ {𝑞 ∈ 𝑋 ∣ 𝑐 ∈ (𝑁‘𝑞)} ⊆ 𝑐)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
139	106, 112, 134, 138	syl12anc 837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
140	18, 139	jca 511	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
141		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑑(𝜑 ∧ 𝑝 ∈ 𝑋)
142		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑑 𝑐 ⊆ ∪ 𝐽
143		nfre1 3285	. . . . . . . . 9 ⊢ Ⅎ𝑑∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)
144	142, 143	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑑(𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))
145	141, 144	nfan 1899	. . . . . . 7 ⊢ Ⅎ𝑑((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)))
146		simplll 775	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
147		simpr 484	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ⊆ 𝑐)
148		simpr1l 1231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ ((𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ 𝐽)
149	148	3anassrs 1361	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ ∪ 𝐽)
150	146, 16	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑋 = ∪ 𝐽)
151	149, 150	sseqtrrd 4021	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ⊆ 𝑋)
152		simplr 769	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑑 ∈ (𝑁‘𝑝))
153		sseq1 4009	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑐))
154	153	3anbi2d 1443	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
155		eleq1w 2824	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑑 ∈ (𝑁‘𝑝)))
156	154, 155	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝))))
157	156	imbi1d 341	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
158		sseq2 4010	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ 𝑐))
159		sseq1 4009	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑋 ↔ 𝑐 ⊆ 𝑋))
160	158, 159	3anbi23d 1441	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋)))
161	160	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
162		eleq1w 2824	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
163	161, 162	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))))
164	163, 10	chvarvv 1998	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
165	157, 164	chvarvv 1998	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋) ∧ 𝑑 ∈ (𝑁‘𝑝)) → 𝑐 ∈ (𝑁‘𝑝))
166	146, 147, 151, 152, 165	syl31anc 1375	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝑁‘𝑝)) ∧ 𝑑 ⊆ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
167	9	neipeltop 23137	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ 𝐽 ↔ (𝑑 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝)))
168	167	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ 𝐽 → ∀𝑝 ∈ 𝑑 𝑑 ∈ (𝑁‘𝑝))
169	168	r19.21bi 3251	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) → 𝑑 ∈ (𝑁‘𝑝))
170	169	anim1i 615	. . . . . . . . . 10 ⊢ (((𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑) ∧ 𝑑 ⊆ 𝑐) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
171	170	anasss 466	. . . . . . . . 9 ⊢ ((𝑑 ∈ 𝐽 ∧ (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → (𝑑 ∈ (𝑁‘𝑝) ∧ 𝑑 ⊆ 𝑐))
172	171	reximi2 3079	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
173	172	ad2antll 729	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝑁‘𝑝)𝑑 ⊆ 𝑐)
174	145, 166, 173	r19.29af 3268	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → 𝑐 ∈ (𝑁‘𝑝))
175	140, 174	impbida 801	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
176	107, 16	eleqtrd 2843	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ ∪ 𝐽)
177		eqid 2737	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
178	177	isneip 23113	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑝 ∈ ∪ 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
179	35, 176, 178	syl2an2r 685	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 ⊆ ∪ 𝐽 ∧ ∃𝑑 ∈ 𝐽 (𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐))))
180	175, 179	bitr4d 282	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑐 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
181	180	eqrdv 2735	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ((nei‘𝐽)‘{𝑝}))
182	181	mpteq2dva 5242	. 2 ⊢ (𝜑 → (𝑝 ∈ 𝑋 ↦ (𝑁‘𝑝)) = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
183	2, 182	eqtrd 2777	1 ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 {crab 3436 Vcvv 3480 ⊆ wss 3951 𝒫 cpw 4600 {csn 4626 ∪ cuni 4907 ↦ cmpt 5225 ⟶wf 6557 ‘cfv 6561 ficfi 9450 Topctop 22899 neicnei 23105

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-om 7888 df-1o 8506 df-2o 8507 df-en 8986 df-fin 8989 df-fi 9451 df-top 22900 df-nei 23106

This theorem is referenced by: neiptopreu 23141 utopsnneiplem 24256

W3C validator