This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem neiptoptop

Description: Lemma for neiptopreu . (Contributed by Thierry Arnoux, 7-Jan-2018)

Ref Expression
Hypotheses neiptop.o ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
neiptop.0 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
neiptop.1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )
neiptop.2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
neiptop.3 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
neiptop.4 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )
neiptop.5 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
Assertion neiptoptop ( 𝜑 → 𝐽 ∈ Top )

Proof

Step Hyp Ref Expression
1 neiptop.o ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
2 neiptop.0 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
3 neiptop.1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )
4 neiptop.2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
5 neiptop.3 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
6 neiptop.4 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )
7 neiptop.5 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
8 uniss ⊢ ( 𝑒 ⊆ 𝐽 → ∪ 𝑒 ⊆ ∪ 𝐽 )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → ∪ 𝑒 ⊆ ∪ 𝐽 )
10 1 2 3 4 5 6 7 neiptopuni ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → 𝑋 = ∪ 𝐽 )
12 9 11 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → ∪ 𝑒 ⊆ 𝑋 )
13 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → 𝜑 )
14 12 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → ∪ 𝑒 ⊆ 𝑋 )
15 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → 𝑝 ∈ ∪ 𝑒 )
16 14 15 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → 𝑝 ∈ 𝑋 )
17 13 16 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) )
18 elssuni ⊢ ( 𝑐 ∈ 𝑒 → 𝑐 ⊆ ∪ 𝑒 )
19 18 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → 𝑐 ⊆ ∪ 𝑒 )
20 17 19 14 3jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → 𝑒 ⊆ 𝐽 )
22 21 sselda ⊢ ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑐 ∈ 𝑒 ) → 𝑐 ∈ 𝐽 )
23 1 neipeltop ⊢ ( 𝑐 ∈ 𝐽 ↔ ( 𝑐 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑐 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) )
24 23 simprbi ⊢ ( 𝑐 ∈ 𝐽 → ∀ 𝑝 ∈ 𝑐 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
25 22 24 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑐 ∈ 𝑒 ) → ∀ 𝑝 ∈ 𝑐 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
26 25 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
27 26 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
28 sseq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ⊆ ∪ 𝑒 ↔ 𝑐 ⊆ ∪ 𝑒 ) )
29 28 3anbi2d ⊢ ( 𝑎 = 𝑐 → ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ) )
30 eleq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) )
31 29 30 anbi12d ⊢ ( 𝑎 = 𝑐 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
32 31 imbi1d ⊢ ( 𝑎 = 𝑐 → ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
33 32 imbi2d ⊢ ( 𝑎 = 𝑐 → ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) ) ↔ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) ) ) )
34 ssidd ⊢ ( 𝜑 → 𝑋 ⊆ 𝑋 )
35 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑋 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
36 1 neipeltop ⊢ ( 𝑋 ∈ 𝐽 ↔ ( 𝑋 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑋 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) ) )
37 34 35 36 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
38 pwexg ⊢ ( 𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V )
39 rabexg ⊢ ( 𝒫 𝑋 ∈ V → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) } ∈ V )
40 37 38 39 3syl ⊢ ( 𝜑 → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) } ∈ V )
41 1 40 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ V )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → 𝐽 ∈ V )
43 42 21 ssexd ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → 𝑒 ∈ V )
44 uniexg ⊢ ( 𝑒 ∈ V → ∪ 𝑒 ∈ V )
45 sseq2 ⊢ ( 𝑏 = ∪ 𝑒 → ( 𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ∪ 𝑒 ) )
46 sseq1 ⊢ ( 𝑏 = ∪ 𝑒 → ( 𝑏 ⊆ 𝑋 ↔ ∪ 𝑒 ⊆ 𝑋 ) )
47 45 46 3anbi23d ⊢ ( 𝑏 = ∪ 𝑒 → ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ) )
48 47 anbi1d ⊢ ( 𝑏 = ∪ 𝑒 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
49 eleq1 ⊢ ( 𝑏 = ∪ 𝑒 → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) )
50 48 49 imbi12d ⊢ ( 𝑏 = ∪ 𝑒 → ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
51 50 3 vtoclg ⊢ ( ∪ 𝑒 ∈ V → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) )
52 43 44 51 3syl ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) )
53 33 52 chvarvv ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) )
54 53 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒 ⊆ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) )
55 20 27 54 mp2and ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) ∧ 𝑐 ∈ 𝑒 ) ∧ 𝑝 ∈ 𝑐 ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) )
56 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) → 𝑝 ∈ ∪ 𝑒 )
57 eluni2 ⊢ ( 𝑝 ∈ ∪ 𝑒 ↔ ∃ 𝑐 ∈ 𝑒 𝑝 ∈ 𝑐 )
58 56 57 sylib ⊢ ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) → ∃ 𝑐 ∈ 𝑒 𝑝 ∈ 𝑐 )
59 55 58 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) ∧ 𝑝 ∈ ∪ 𝑒 ) → ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) )
60 59 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → ∀ 𝑝 ∈ ∪ 𝑒 ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) )
61 1 neipeltop ⊢ ( ∪ 𝑒 ∈ 𝐽 ↔ ( ∪ 𝑒 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ∪ 𝑒 ∪ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) )
62 12 60 61 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐽 ) → ∪ 𝑒 ∈ 𝐽 )
63 62 ex ⊢ ( 𝜑 → ( 𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽 ) )
64 63 alrimiv ⊢ ( 𝜑 → ∀ 𝑒 ( 𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽 ) )
65 inss1 ⊢ ( 𝑒 ∩ 𝑓 ) ⊆ 𝑒
66 1 neipeltop ⊢ ( 𝑒 ∈ 𝐽 ↔ ( 𝑒 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑒 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ) )
67 66 simplbi ⊢ ( 𝑒 ∈ 𝐽 → 𝑒 ⊆ 𝑋 )
68 67 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) → 𝑒 ⊆ 𝑋 )
69 65 68 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) → ( 𝑒 ∩ 𝑓 ) ⊆ 𝑋 )
70 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝜑 )
71 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑒 ∈ 𝐽 )
72 71 67 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑒 ⊆ 𝑋 )
73 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) )
74 73 elin1d ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑝 ∈ 𝑒 )
75 72 74 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑝 ∈ 𝑋 )
76 70 75 4 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
77 fvex ⊢ ( 𝑁 ‘ 𝑝 ) ∈ V
78 66 simprbi ⊢ ( 𝑒 ∈ 𝐽 → ∀ 𝑝 ∈ 𝑒 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) )
79 78 r19.21bi ⊢ ( ( 𝑒 ∈ 𝐽 ∧ 𝑝 ∈ 𝑒 ) → 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) )
80 71 74 79 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) )
81 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑓 ∈ 𝐽 )
82 73 elin2d ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑝 ∈ 𝑓 )
83 1 neipeltop ⊢ ( 𝑓 ∈ 𝐽 ↔ ( 𝑓 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑓 𝑓 ∈ ( 𝑁 ‘ 𝑝 ) ) )
84 83 simprbi ⊢ ( 𝑓 ∈ 𝐽 → ∀ 𝑝 ∈ 𝑓 𝑓 ∈ ( 𝑁 ‘ 𝑝 ) )
85 84 r19.21bi ⊢ ( ( 𝑓 ∈ 𝐽 ∧ 𝑝 ∈ 𝑓 ) → 𝑓 ∈ ( 𝑁 ‘ 𝑝 ) )
86 81 82 85 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → 𝑓 ∈ ( 𝑁 ‘ 𝑝 ) )
87 inelfi ⊢ ( ( ( 𝑁 ‘ 𝑝 ) ∈ V ∧ 𝑒 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝑓 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑒 ∩ 𝑓 ) ∈ ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) )
88 77 80 86 87 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → ( 𝑒 ∩ 𝑓 ) ∈ ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) )
89 76 88 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) ∧ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ) → ( 𝑒 ∩ 𝑓 ) ∈ ( 𝑁 ‘ 𝑝 ) )
90 89 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) → ∀ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ( 𝑒 ∩ 𝑓 ) ∈ ( 𝑁 ‘ 𝑝 ) )
91 1 neipeltop ⊢ ( ( 𝑒 ∩ 𝑓 ) ∈ 𝐽 ↔ ( ( 𝑒 ∩ 𝑓 ) ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ( 𝑒 ∩ 𝑓 ) ( 𝑒 ∩ 𝑓 ) ∈ ( 𝑁 ‘ 𝑝 ) ) )
92 69 90 91 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) ∧ 𝑓 ∈ 𝐽 ) → ( 𝑒 ∩ 𝑓 ) ∈ 𝐽 )
93 92 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐽 ) → ∀ 𝑓 ∈ 𝐽 ( 𝑒 ∩ 𝑓 ) ∈ 𝐽 )
94 93 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝐽 ∀ 𝑓 ∈ 𝐽 ( 𝑒 ∩ 𝑓 ) ∈ 𝐽 )
95 istopg ⊢ ( 𝐽 ∈ V → ( 𝐽 ∈ Top ↔ ( ∀ 𝑒 ( 𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽 ) ∧ ∀ 𝑒 ∈ 𝐽 ∀ 𝑓 ∈ 𝐽 ( 𝑒 ∩ 𝑓 ) ∈ 𝐽 ) ) )
96 41 95 syl ⊢ ( 𝜑 → ( 𝐽 ∈ Top ↔ ( ∀ 𝑒 ( 𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽 ) ∧ ∀ 𝑒 ∈ 𝐽 ∀ 𝑓 ∈ 𝐽 ( 𝑒 ∩ 𝑓 ) ∈ 𝐽 ) ) )
97 64 94 96 mpbir2and ⊢ ( 𝜑 → 𝐽 ∈ Top )