Theorem neiptoptop 22190

Description: Lemma for neiptopreu 22192. (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 4844	. . . . . . 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 22189	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
11	10	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑋 = ∪ 𝐽)
12	2, 11	sseqtrrd 3958	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ⊆ 𝑋)
13		simp-4l 779	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝜑)
14	12	ad3antrrr 726	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ⊆ 𝑋)
15		simpllr 772	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ ∪ 𝑒)
16	14, 15	sseldd 3918	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋)
17	13, 16	jca 511	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
18		elssuni 4868	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑒 → 𝑐 ⊆ ∪ 𝑒)
19	18	ad2antlr 723	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ⊆ ∪ 𝑒)
20	17, 19, 14	3jca 1126	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋))
21		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ⊆ 𝐽)
22	21	sselda 3917	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → 𝑐 ∈ 𝐽)
23	3	neipeltop 22188	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐽 ↔ (𝑐 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝)))
24	23	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐽 → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))
25	22, 24	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))
26	25	r19.21bi 3132	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
27	26	adantllr 715	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
28		sseq1 3942	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ ∪ 𝑒 ↔ 𝑐 ⊆ ∪ 𝑒))
29	28	3anbi2d 1439	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋)))
30		eleq1 2826	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
31	29, 30	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
32	31	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))
33	32	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))))
34		ssidd 3940	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ⊆ 𝑋)
35	9	ralrimiva 3107	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝))
36	3	neipeltop 22188	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝)))
37	34, 35, 36	sylanbrc 582	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ 𝐽)
38		pwexg 5296	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
39		rabexg 5250	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑋 ∈ V → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V)
40	37, 38, 39	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V)
41	3, 40	eqeltrid 2843	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ V)
42	41	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝐽 ∈ V)
43	42, 21	ssexd 5243	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ∈ V)
44		uniexg 7571	. . . . . . . . . . 11 ⊢ (𝑒 ∈ V → ∪ 𝑒 ∈ V)
45		sseq2 3943	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∪ 𝑒 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ∪ 𝑒))
46		sseq1 3942	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∪ 𝑒 → (𝑏 ⊆ 𝑋 ↔ ∪ 𝑒 ⊆ 𝑋))
47	45, 46	3anbi23d 1437	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ∪ 𝑒 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋)))
48	47	anbi1d 629	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∪ 𝑒 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
49		eleq1 2826	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∪ 𝑒 → (𝑏 ∈ (𝑁‘𝑝) ↔ ∪ 𝑒 ∈ (𝑁‘𝑝)))
50	48, 49	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑏 = ∪ 𝑒 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))
51	50, 5	vtoclg 3495	. . . . . . . . . . 11 ⊢ (∪ 𝑒 ∈ V → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
52	43, 44, 51	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
53	33, 52	chvarvv 2003	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
54	53	ad3antrrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
55	20, 27, 54	mp2and 695	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ∈ (𝑁‘𝑝))
56		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → 𝑝 ∈ ∪ 𝑒)
57		eluni2 4840	. . . . . . . 8 ⊢ (𝑝 ∈ ∪ 𝑒 ↔ ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐)
58	56, 57	sylib 217	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐)
59	55, 58	r19.29a 3217	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∪ 𝑒 ∈ (𝑁‘𝑝))
60	59	ralrimiva 3107	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝))
61	3	neipeltop 22188	. . . . 5 ⊢ (∪ 𝑒 ∈ 𝐽 ↔ (∪ 𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝)))
62	12, 60, 61	sylanbrc 582	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ∈ 𝐽)
63	62	ex 412	. . 3 ⊢ (𝜑 → (𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽))
64	63	alrimiv 1931	. 2 ⊢ (𝜑 → ∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽))
65		inss1 4159	. . . . . 6 ⊢ (𝑒 ∩ 𝑓) ⊆ 𝑒
66	3	neipeltop 22188	. . . . . . . 8 ⊢ (𝑒 ∈ 𝐽 ↔ (𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝)))
67	66	simplbi 497	. . . . . . 7 ⊢ (𝑒 ∈ 𝐽 → 𝑒 ⊆ 𝑋)
68	67	ad2antlr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → 𝑒 ⊆ 𝑋)
69	65, 68	sstrid 3928	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ⊆ 𝑋)
70		simplll 771	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝜑)
71		simpllr 772	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ 𝐽)
72	71, 67	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ⊆ 𝑋)
73		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ (𝑒 ∩ 𝑓))
74	73	elin1d 4128	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑒)
75	72, 74	sseldd 3918	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑋)
76	70, 75, 6	syl2anc 583	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
77		fvex 6769	. . . . . . . 8 ⊢ (𝑁‘𝑝) ∈ V
78	66	simprbi 496	. . . . . . . . . 10 ⊢ (𝑒 ∈ 𝐽 → ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝))
79	78	r19.21bi 3132	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝐽 ∧ 𝑝 ∈ 𝑒) → 𝑒 ∈ (𝑁‘𝑝))
80	71, 74, 79	syl2anc 583	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ (𝑁‘𝑝))
81		simplr 765	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ 𝐽)
82	73	elin2d 4129	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑓)
83	3	neipeltop 22188	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝐽 ↔ (𝑓 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝)))
84	83	simprbi 496	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐽 → ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝))
85	84	r19.21bi 3132	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐽 ∧ 𝑝 ∈ 𝑓) → 𝑓 ∈ (𝑁‘𝑝))
86	81, 82, 85	syl2anc 583	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ (𝑁‘𝑝))
87		inelfi 9107	. . . . . . . 8 ⊢ (((𝑁‘𝑝) ∈ V ∧ 𝑒 ∈ (𝑁‘𝑝) ∧ 𝑓 ∈ (𝑁‘𝑝)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝)))
88	77, 80, 86, 87	mp3an2i 1464	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝)))
89	76, 88	sseldd 3918	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))
90	89	ralrimiva 3107	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))
91	3	neipeltop 22188	. . . . 5 ⊢ ((𝑒 ∩ 𝑓) ∈ 𝐽 ↔ ((𝑒 ∩ 𝑓) ⊆ 𝑋 ∧ ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝)))
92	69, 90, 91	sylanbrc 582	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ∈ 𝐽)
93	92	ralrimiva 3107	. . 3 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐽) → ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)
94	93	ralrimiva 3107	. 2 ⊢ (𝜑 → ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)
95		istopg 21952	. . 3 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)))
96	41, 95	syl 17	. 2 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)))
97	64, 94, 96	mpbir2and 709	1 ⊢ (𝜑 → 𝐽 ∈ Top)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1537   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4530  ∪ cuni 4836  ⟶wf 6414  ‘cfv 6418  ficfi 9099  Topctop 21950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-om 7688  df-1o 8267  df-en 8692  df-fin 8695  df-fi 9100  df-top 21951

This theorem is referenced by:  neiptopnei  22191  neiptopreu  22192