Theorem neiptoptop 23139

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
neiptoptop	⊢ (𝜑 → 𝐽 ∈ Top)

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

Allowed substitution hints:   𝜑(𝑞)   𝐽(𝑞,𝑏)   𝑁(𝑞,𝑝)   𝑋(𝑞)

Proof of Theorem neiptoptop

Dummy variables 𝑐 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniss 4915	. . . . . . 7 ⊢ (𝑒 ⊆ 𝐽 → ∪ 𝑒 ⊆ ∪ 𝐽)
2	1	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ⊆ ∪ 𝐽)
3		neiptop.o	. . . . . . . 8 ⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}
4		neiptop.0	. . . . . . . 8 ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
5		neiptop.1	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
6		neiptop.2	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
7		neiptop.3	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
8		neiptop.4	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
9		neiptop.5	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
10	3, 4, 5, 6, 7, 8, 9	neiptopuni 23138	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
11	10	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑋 = ∪ 𝐽)
12	2, 11	sseqtrrd 4021	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ⊆ 𝑋)
13		simp-4l 783	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝜑)
14	12	ad3antrrr 730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ⊆ 𝑋)
15		simpllr 776	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ ∪ 𝑒)
16	14, 15	sseldd 3984	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋)
17	13, 16	jca 511	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
18		elssuni 4937	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑒 → 𝑐 ⊆ ∪ 𝑒)
19	18	ad2antlr 727	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ⊆ ∪ 𝑒)
20	17, 19, 14	3jca 1129	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋))
21		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ⊆ 𝐽)
22	21	sselda 3983	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → 𝑐 ∈ 𝐽)
23	3	neipeltop 23137	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐽 ↔ (𝑐 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝)))
24	23	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐽 → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))
25	22, 24	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))
26	25	r19.21bi 3251	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
27	26	adantllr 719	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
28		sseq1 4009	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ ∪ 𝑒 ↔ 𝑐 ⊆ ∪ 𝑒))
29	28	3anbi2d 1443	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋)))
30		eleq1 2829	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
31	29, 30	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
32	31	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))
33	32	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))))
34		ssidd 4007	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ⊆ 𝑋)
35	9	ralrimiva 3146	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝))
36	3	neipeltop 23137	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝)))
37	34, 35, 36	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ 𝐽)
38		pwexg 5378	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
39		rabexg 5337	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑋 ∈ V → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V)
40	37, 38, 39	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V)
41	3, 40	eqeltrid 2845	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ V)
42	41	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝐽 ∈ V)
43	42, 21	ssexd 5324	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ∈ V)
44		uniexg 7760	. . . . . . . . . . 11 ⊢ (𝑒 ∈ V → ∪ 𝑒 ∈ V)
45		sseq2 4010	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∪ 𝑒 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ∪ 𝑒))
46		sseq1 4009	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∪ 𝑒 → (𝑏 ⊆ 𝑋 ↔ ∪ 𝑒 ⊆ 𝑋))
47	45, 46	3anbi23d 1441	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ∪ 𝑒 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋)))
48	47	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∪ 𝑒 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
49		eleq1 2829	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∪ 𝑒 → (𝑏 ∈ (𝑁‘𝑝) ↔ ∪ 𝑒 ∈ (𝑁‘𝑝)))
50	48, 49	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑏 = ∪ 𝑒 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))
51	50, 5	vtoclg 3554	. . . . . . . . . . 11 ⊢ (∪ 𝑒 ∈ V → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
52	43, 44, 51	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
53	33, 52	chvarvv 1998	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
54	53	ad3antrrr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
55	20, 27, 54	mp2and 699	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ∈ (𝑁‘𝑝))
56		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → 𝑝 ∈ ∪ 𝑒)
57		eluni2 4911	. . . . . . . 8 ⊢ (𝑝 ∈ ∪ 𝑒 ↔ ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐)
58	56, 57	sylib 218	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐)
59	55, 58	r19.29a 3162	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∪ 𝑒 ∈ (𝑁‘𝑝))
60	59	ralrimiva 3146	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝))
61	3	neipeltop 23137	. . . . 5 ⊢ (∪ 𝑒 ∈ 𝐽 ↔ (∪ 𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝)))
62	12, 60, 61	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ∈ 𝐽)
63	62	ex 412	. . 3 ⊢ (𝜑 → (𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽))
64	63	alrimiv 1927	. 2 ⊢ (𝜑 → ∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽))
65		inss1 4237	. . . . . 6 ⊢ (𝑒 ∩ 𝑓) ⊆ 𝑒
66	3	neipeltop 23137	. . . . . . . 8 ⊢ (𝑒 ∈ 𝐽 ↔ (𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝)))
67	66	simplbi 497	. . . . . . 7 ⊢ (𝑒 ∈ 𝐽 → 𝑒 ⊆ 𝑋)
68	67	ad2antlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → 𝑒 ⊆ 𝑋)
69	65, 68	sstrid 3995	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ⊆ 𝑋)
70		simplll 775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝜑)
71		simpllr 776	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ 𝐽)
72	71, 67	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ⊆ 𝑋)
73		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ (𝑒 ∩ 𝑓))
74	73	elin1d 4204	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑒)
75	72, 74	sseldd 3984	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑋)
76	70, 75, 6	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
77		fvex 6919	. . . . . . . 8 ⊢ (𝑁‘𝑝) ∈ V
78	66	simprbi 496	. . . . . . . . . 10 ⊢ (𝑒 ∈ 𝐽 → ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝))
79	78	r19.21bi 3251	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝐽 ∧ 𝑝 ∈ 𝑒) → 𝑒 ∈ (𝑁‘𝑝))
80	71, 74, 79	syl2anc 584	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ (𝑁‘𝑝))
81		simplr 769	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ 𝐽)
82	73	elin2d 4205	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑓)
83	3	neipeltop 23137	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝐽 ↔ (𝑓 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝)))
84	83	simprbi 496	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐽 → ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝))
85	84	r19.21bi 3251	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐽 ∧ 𝑝 ∈ 𝑓) → 𝑓 ∈ (𝑁‘𝑝))
86	81, 82, 85	syl2anc 584	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ (𝑁‘𝑝))
87		inelfi 9458	. . . . . . . 8 ⊢ (((𝑁‘𝑝) ∈ V ∧ 𝑒 ∈ (𝑁‘𝑝) ∧ 𝑓 ∈ (𝑁‘𝑝)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝)))
88	77, 80, 86, 87	mp3an2i 1468	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝)))
89	76, 88	sseldd 3984	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))
90	89	ralrimiva 3146	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))
91	3	neipeltop 23137	. . . . 5 ⊢ ((𝑒 ∩ 𝑓) ∈ 𝐽 ↔ ((𝑒 ∩ 𝑓) ⊆ 𝑋 ∧ ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝)))
92	69, 90, 91	sylanbrc 583	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ∈ 𝐽)
93	92	ralrimiva 3146	. . 3 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐽) → ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)
94	93	ralrimiva 3146	. 2 ⊢ (𝜑 → ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)
95		istopg 22901	. . 3 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)))
96	41, 95	syl 17	. 2 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)))
97	64, 94, 96	mpbir2and 713	1 ⊢ (𝜑 → 𝐽 ∈ Top)

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

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-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-rab 3437  df-v 3482  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-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-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

This theorem is referenced by:  neiptopnei  23140  neiptopreu  23141