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