neiptoptop - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > neiptoptop		Structured version Visualization version GIF version

Theorem neiptoptop 22957

Description: Lemma for neiptopreu 22959. (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 4907	. . . . . . 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 22956	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
11	10	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑋 = ∪ 𝐽)
12	2, 11	sseqtrrd 4015	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ⊆ 𝑋)
13		simp-4l 780	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝜑)
14	12	ad3antrrr 727	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ⊆ 𝑋)
15		simpllr 773	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ ∪ 𝑒)
16	14, 15	sseldd 3975	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋)
17	13, 16	jca 511	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋))
18		elssuni 4931	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑒 → 𝑐 ⊆ ∪ 𝑒)
19	18	ad2antlr 724	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ⊆ ∪ 𝑒)
20	17, 19, 14	3jca 1125	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋))
21		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ⊆ 𝐽)
22	21	sselda 3974	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → 𝑐 ∈ 𝐽)
23	3	neipeltop 22955	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐽 ↔ (𝑐 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝)))
24	23	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐽 → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))
25	22, 24	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))
26	25	r19.21bi 3240	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
27	26	adantllr 716	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝))
28		sseq1 3999	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ ∪ 𝑒 ↔ 𝑐 ⊆ ∪ 𝑒))
29	28	3anbi2d 1437	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋)))
30		eleq1 2813	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝)))
31	29, 30	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝))))
32	31	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))
33	32	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))))
34		ssidd 3997	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ⊆ 𝑋)
35	9	ralrimiva 3138	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝))
36	3	neipeltop 22955	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝)))
37	34, 35, 36	sylanbrc 582	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ 𝐽)
38		pwexg 5366	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V)
39		rabexg 5321	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑋 ∈ V → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V)
40	37, 38, 39	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V)
41	3, 40	eqeltrid 2829	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ V)
42	41	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝐽 ∈ V)
43	42, 21	ssexd 5314	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ∈ V)
44		uniexg 7723	. . . . . . . . . . 11 ⊢ (𝑒 ∈ V → ∪ 𝑒 ∈ V)
45		sseq2 4000	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∪ 𝑒 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ∪ 𝑒))
46		sseq1 3999	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∪ 𝑒 → (𝑏 ⊆ 𝑋 ↔ ∪ 𝑒 ⊆ 𝑋))
47	45, 46	3anbi23d 1435	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ∪ 𝑒 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋)))
48	47	anbi1d 629	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∪ 𝑒 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝))))
49		eleq1 2813	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∪ 𝑒 → (𝑏 ∈ (𝑁‘𝑝) ↔ ∪ 𝑒 ∈ (𝑁‘𝑝)))
50	48, 49	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑏 = ∪ 𝑒 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))
51	50, 5	vtoclg 3535	. . . . . . . . . . 11 ⊢ (∪ 𝑒 ∈ V → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
52	43, 44, 51	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
53	33, 52	chvarvv 1994	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
54	53	ad3antrrr 727	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))
55	20, 27, 54	mp2and 696	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ∈ (𝑁‘𝑝))
56		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → 𝑝 ∈ ∪ 𝑒)
57		eluni2 4903	. . . . . . . 8 ⊢ (𝑝 ∈ ∪ 𝑒 ↔ ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐)
58	56, 57	sylib 217	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐)
59	55, 58	r19.29a 3154	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∪ 𝑒 ∈ (𝑁‘𝑝))
60	59	ralrimiva 3138	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝))
61	3	neipeltop 22955	. . . . 5 ⊢ (∪ 𝑒 ∈ 𝐽 ↔ (∪ 𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝)))
62	12, 60, 61	sylanbrc 582	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ∈ 𝐽)
63	62	ex 412	. . 3 ⊢ (𝜑 → (𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽))
64	63	alrimiv 1922	. 2 ⊢ (𝜑 → ∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽))
65		inss1 4220	. . . . . 6 ⊢ (𝑒 ∩ 𝑓) ⊆ 𝑒
66	3	neipeltop 22955	. . . . . . . 8 ⊢ (𝑒 ∈ 𝐽 ↔ (𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝)))
67	66	simplbi 497	. . . . . . 7 ⊢ (𝑒 ∈ 𝐽 → 𝑒 ⊆ 𝑋)
68	67	ad2antlr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → 𝑒 ⊆ 𝑋)
69	65, 68	sstrid 3985	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ⊆ 𝑋)
70		simplll 772	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝜑)
71		simpllr 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ 𝐽)
72	71, 67	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ⊆ 𝑋)
73		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ (𝑒 ∩ 𝑓))
74	73	elin1d 4190	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑒)
75	72, 74	sseldd 3975	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑋)
76	70, 75, 6	syl2anc 583	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
77		fvex 6894	. . . . . . . 8 ⊢ (𝑁‘𝑝) ∈ V
78	66	simprbi 496	. . . . . . . . . 10 ⊢ (𝑒 ∈ 𝐽 → ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝))
79	78	r19.21bi 3240	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝐽 ∧ 𝑝 ∈ 𝑒) → 𝑒 ∈ (𝑁‘𝑝))
80	71, 74, 79	syl2anc 583	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ (𝑁‘𝑝))
81		simplr 766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ 𝐽)
82	73	elin2d 4191	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑓)
83	3	neipeltop 22955	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝐽 ↔ (𝑓 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝)))
84	83	simprbi 496	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐽 → ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝))
85	84	r19.21bi 3240	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐽 ∧ 𝑝 ∈ 𝑓) → 𝑓 ∈ (𝑁‘𝑝))
86	81, 82, 85	syl2anc 583	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ (𝑁‘𝑝))
87		inelfi 9409	. . . . . . . 8 ⊢ (((𝑁‘𝑝) ∈ V ∧ 𝑒 ∈ (𝑁‘𝑝) ∧ 𝑓 ∈ (𝑁‘𝑝)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝)))
88	77, 80, 86, 87	mp3an2i 1462	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝)))
89	76, 88	sseldd 3975	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))
90	89	ralrimiva 3138	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))
91	3	neipeltop 22955	. . . . 5 ⊢ ((𝑒 ∩ 𝑓) ∈ 𝐽 ↔ ((𝑒 ∩ 𝑓) ⊆ 𝑋 ∧ ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝)))
92	69, 90, 91	sylanbrc 582	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ∈ 𝐽)
93	92	ralrimiva 3138	. . 3 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐽) → ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)
94	93	ralrimiva 3138	. 2 ⊢ (𝜑 → ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)
95		istopg 22719	. . 3 ⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)))
96	41, 95	syl 17	. 2 ⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽)))
97	64, 94, 96	mpbir2and 710	1 ⊢ (𝜑 → 𝐽 ∈ Top)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1084 ∀wal 1531 = wceq 1533 ∈ wcel 2098 ∀wral 3053 ∃wrex 3062 {crab 3424 Vcvv 3466 ∩ cin 3939 ⊆ wss 3940 𝒫 cpw 4594 ∪ cuni 4899 ⟶wf 6529 ‘cfv 6533 ficfi 9401 Topctop 22717

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-int 4941 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-om 7849 df-1o 8461 df-en 8936 df-fin 8939 df-fi 9402 df-top 22718

This theorem is referenced by: neiptopnei 22958 neiptopreu 22959

W3C validator