Theorem neiptoptop 23114

Description: Lemma for neiptopreu 23116. (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 4846	. . . . . . 7 ⊢ (𝑒 ⊆ 𝐽 → ∪ 𝑒 ⊆ ∪ 𝐽)
2	1	adantl 482	. . . . . 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 23113	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
11	10	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑋 = ∪ 𝐽)
12	2, 11	sseqtrrd 3952	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ⊆ 𝑋)
13		simp-4l 788	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝜑)
14	12	ad3antrrr 736	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ⊆ 𝑋)
15		simpllr 781	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ ∪ 𝑒)
16	14, 15	sseldd 3916	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋)
17	13, 16	jca 516	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
18		elssuni 4869	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑒 → 𝑐 ⊆ ∪ 𝑒)
19	18	ad2antlr 733	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ⊆ ∪ 𝑒)
20	17, 19, 14	3jca 1134	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋))
21		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ⊆ 𝐽)
22	21	sselda 3915	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → 𝑐 ∈ 𝐽)
23	3	neipeltop 23112	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐽 ↔ (𝑐 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝)))
24	23	simprbi 498	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐽 → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))
25	22, 24	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))
26	25	r19.21bi 3231	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
27	26	adantllr 725	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
28		sseq1 3940	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ ∪ 𝑒 ↔ 𝑐 ⊆ ∪ 𝑒))
29	28	3anbi2d 1449	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋)))
30		eleq1 2827	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
31	29, 30	anbi12d 638	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
32	31	imbi1d 342	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))
33	32	imbi2d 341	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))))
34		ssidd 3938	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ⊆ 𝑋)
35	9	ralrimiva 3131	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝))
36	3	neipeltop 23112	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝)))
37	34, 35, 36	sylanbrc 589	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ 𝐽)
38		pwexg 5307	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
39		rabexg 5265	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑋 ∈ V → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V)
40	37, 38, 39	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V)
41	3, 40	eqeltrid 2843	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ V)
42	41	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝐽 ∈ V)
43	42, 21	ssexd 5252	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ∈ V)
44		uniexg 7683	. . . . . . . . . . 11 ⊢ (𝑒 ∈ V → ∪ 𝑒 ∈ V)
45		sseq2 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∪ 𝑒 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ∪ 𝑒))
46		sseq1 3940	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∪ 𝑒 → (𝑏 ⊆ 𝑋 ↔ ∪ 𝑒 ⊆ 𝑋))
47	45, 46	3anbi23d 1447	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ∪ 𝑒 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋)))
48	47	anbi1d 637	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∪ 𝑒 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
49		eleq1 2827	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∪ 𝑒 → (𝑏 ∈ (𝑁‘𝑝) ↔ ∪ 𝑒 ∈ (𝑁‘𝑝)))
50	48, 49	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑏 = ∪ 𝑒 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))
51	50, 5	vtoclg 3500	. . . . . . . . . . 11 ⊢ (∪ 𝑒 ∈ V → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
52	43, 44, 51	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
53	33, 52	chvarvv 1996	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
54	53	ad3antrrr 736	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
55	20, 27, 54	mp2and 705	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ∈ (𝑁‘𝑝))
56		eluni2 4842	. . . . . . . 8 ⊢ (𝑝 ∈ ∪ 𝑒 ↔ ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐)
57	56	bilani 505	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐)
58	55, 57	r19.29a 3147	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∪ 𝑒 ∈ (𝑁‘𝑝))
59	58	ralrimiva 3131	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝))
60	3	neipeltop 23112	. . . . 5 ⊢ (∪ 𝑒 ∈ 𝐽 ↔ (∪ 𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝)))
61	12, 59, 60	sylanbrc 589	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ∈ 𝐽)
62	61	ex 413	. . 3 ⊢ (𝜑 → (𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽))
63	62	alrimiv 1934	. 2 ⊢ (𝜑 → ∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽))
64		inss1 4165	. . . . . 6 ⊢ (𝑒 ∩ 𝑓) ⊆ 𝑒
65	3	neipeltop 23112	. . . . . . . 8 ⊢ (𝑒 ∈ 𝐽 ↔ (𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝)))
66	65	simplbi 497	. . . . . . 7 ⊢ (𝑒 ∈ 𝐽 → 𝑒 ⊆ 𝑋)
67	66	ad2antlr 733	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → 𝑒 ⊆ 𝑋)
68	64, 67	sstrid 3926	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ⊆ 𝑋)
69		simplll 780	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝜑)
70		simpllr 781	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ 𝐽)
71	70, 66	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ⊆ 𝑋)
72		simpr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ (𝑒 ∩ 𝑓))
73	72	elin1d 4133	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑒)
74	71, 73	sseldd 3916	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑋)
75	69, 74, 6	syl2anc 590	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
76		fvex 6840	. . . . . . . 8 ⊢ (𝑁‘𝑝) ∈ V
77	65	simprbi 498	. . . . . . . . . 10 ⊢ (𝑒 ∈ 𝐽 → ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝))
78	77	r19.21bi 3231	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝐽 ∧ 𝑝 ∈ 𝑒) → 𝑒 ∈ (𝑁‘𝑝))
79	70, 73, 78	syl2anc 590	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ (𝑁‘𝑝))
80		simplr 774	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ 𝐽)
81	72	elin2d 4134	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑓)
82	3	neipeltop 23112	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝐽 ↔ (𝑓 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝)))
83	82	simprbi 498	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐽 → ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝))
84	83	r19.21bi 3231	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐽 ∧ 𝑝 ∈ 𝑓) → 𝑓 ∈ (𝑁‘𝑝))
85	80, 81, 84	syl2anc 590	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ (𝑁‘𝑝))
86		inelfi 9321	. . . . . . . 8 ⊢ (((𝑁‘𝑝) ∈ V ∧ 𝑒 ∈ (𝑁‘𝑝) ∧ 𝑓 ∈ (𝑁‘𝑝)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝)))
87	76, 79, 85, 86	mp3an2i 1474	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝)))
88	75, 87	sseldd 3916	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))
89	88	ralrimiva 3131	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))
90	3	neipeltop 23112	. . . . 5 ⊢ ((𝑒 ∩ 𝑓) ∈ 𝐽 ↔ ((𝑒 ∩ 𝑓) ⊆ 𝑋 ∧ ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝)))
91	68, 89, 90	sylanbrc 589	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ∈ 𝐽)
92	91	ralrimiva 3131	. . 3 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐽) → ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)
93	92	ralrimiva 3131	. 2 ⊢ (𝜑 → ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)
94		istopg 22878	. . 3 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)))
95	41, 94	syl 17	. 2 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)))
96	63, 93, 95	mpbir2and 719	1 ⊢ (𝜑 → 𝐽 ∈ Top)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092  ∀wal 1545   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063  {crab 3391  Vcvv 3431   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4529  ∪ cuni 4838  ⟶wf 6481  ‘cfv 6485  ficfi 9313  Topctop 22876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-om 7807  df-1o 8395  df-2o 8396  df-en 8884  df-fin 8887  df-fi 9314  df-top 22877

This theorem is referenced by:  neiptopnei  23115  neiptopreu  23116