Metamath Proof Explorer

Theorem flimclslem

Description: Lemma for flimcls . (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flimcls.2 ⊢ 𝐹 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) )
Assertion flimclslem ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 flimcls.2 ⊢ 𝐹 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) )
2 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
3 2 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐽 ∈ Top )
4 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
5 4 neisspw ⊢ ( 𝐽 ∈ Top → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝒫 ∪ 𝐽 )
6 3 5 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝒫 ∪ 𝐽 )
7 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
8 7 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑋 = ∪ 𝐽 )
9 8 pweqd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝒫 𝑋 = 𝒫 ∪ 𝐽 )
10 6 9 sseqtrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝒫 𝑋 )
11 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
12 elpw2g ⊢ ( 𝑋 ∈ 𝐽 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
13 11 12 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
14 13 biimpar ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
15 14 3adant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ 𝒫 𝑋 )
16 15 snssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → { 𝑆 } ⊆ 𝒫 𝑋 )
17 10 16 unssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ⊆ 𝒫 𝑋 )
18 ssun2 ⊢ { 𝑆 } ⊆ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } )
19 11 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑋 ∈ 𝐽 )
20 simp2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑋 )
21 19 20 ssexd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ V )
22 21 snn0d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → { 𝑆 } ≠ ∅ )
23 ssn0 ⊢ ( ( { 𝑆 } ⊆ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ∧ { 𝑆 } ≠ ∅ ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ≠ ∅ )
24 18 22 23 sylancr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ≠ ∅ )
25 20 8 sseqtrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ∪ 𝐽 )
26 simp3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
27 4 neindisj ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) → ( 𝑥 ∩ 𝑆 ) ≠ ∅ )
28 27 expr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
29 3 25 26 28 syl21anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
30 29 imp ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝑥 ∩ 𝑆 ) ≠ ∅ )
31 elsni ⊢ ( 𝑦 ∈ { 𝑆 } → 𝑦 = 𝑆 )
32 31 ineq2d ⊢ ( 𝑦 ∈ { 𝑆 } → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ 𝑆 ) )
33 32 neeq1d ⊢ ( 𝑦 ∈ { 𝑆 } → ( ( 𝑥 ∩ 𝑦 ) ≠ ∅ ↔ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
34 30 33 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝑦 ∈ { 𝑆 } → ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) )
35 34 ralrimiv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ∀ 𝑦 ∈ { 𝑆 } ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
36 35 ralrimiva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑦 ∈ { 𝑆 } ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
37 simp1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
38 4 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
39 3 25 38 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
40 39 26 sseldd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐴 ∈ ∪ 𝐽 )
41 40 8 eleqtrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐴 ∈ 𝑋 )
42 41 snssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → { 𝐴 } ⊆ 𝑋 )
43 snnzg ⊢ ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → { 𝐴 } ≠ ∅ )
44 43 3ad2ant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → { 𝐴 } ≠ ∅ )
45 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ∧ { 𝐴 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
46 37 42 44 45 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
47 filfbas ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( fBas ‘ 𝑋 ) )
48 46 47 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( fBas ‘ 𝑋 ) )
49 ne0i ⊢ ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ≠ ∅ )
50 49 3ad2ant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ≠ ∅ )
51 cls0 ⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ ∅ ) = ∅ )
52 3 51 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ ∅ ) = ∅ )
53 50 52 neeqtrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ≠ ( ( cls ‘ 𝐽 ) ‘ ∅ ) )
54 fveq2 ⊢ ( 𝑆 = ∅ → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( ( cls ‘ 𝐽 ) ‘ ∅ ) )
55 54 necon3i ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ≠ ( ( cls ‘ 𝐽 ) ‘ ∅ ) → 𝑆 ≠ ∅ )
56 53 55 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ≠ ∅ )
57 snfbas ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ 𝑋 ∈ 𝐽 ) → { 𝑆 } ∈ ( fBas ‘ 𝑋 ) )
58 20 56 19 57 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → { 𝑆 } ∈ ( fBas ‘ 𝑋 ) )
59 fbunfip ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑆 } ∈ ( fBas ‘ 𝑋 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ↔ ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑦 ∈ { 𝑆 } ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) )
60 48 58 59 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ↔ ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑦 ∈ { 𝑆 } ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) )
61 36 60 mpbird ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) )
62 fsubbas ⊢ ( 𝑋 ∈ 𝐽 → ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ⊆ 𝒫 𝑋 ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) )
63 19 62 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ⊆ 𝒫 𝑋 ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) )
64 17 24 61 63 mpbir3and ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ∈ ( fBas ‘ 𝑋 ) )
65 fgcl ⊢ ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
66 64 65 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
67 1 66 eqeltrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
68 fvex ⊢ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ V
69 snex ⊢ { 𝑆 } ∈ V
70 68 69 unex ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ∈ V
71 ssfii ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ∈ V → ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ⊆ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) )
72 70 71 ax-mp ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ⊆ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) )
73 ssfg ⊢ ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) )
74 64 73 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) )
75 74 1 sseqtrrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ⊆ 𝐹 )
76 72 75 sstrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ⊆ 𝐹 )
77 snssg ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ↔ { 𝑆 } ⊆ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) )
78 21 77 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑆 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ↔ { 𝑆 } ⊆ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) )
79 18 78 mpbiri ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) )
80 76 79 sseldd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ 𝐹 )
81 76 unssad ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 )
82 elflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
83 37 67 82 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
84 41 81 83 mpbir2and ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) )
85 67 80 84 3jca ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) )