| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | flimcls.2 | . . 3
⊢ 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) | 
| 2 |  | topontop 22920 | . . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | 
| 3 | 2 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top) | 
| 4 |  | eqid 2736 | . . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 5 | 4 | neisspw 23116 | . . . . . . . 8
⊢ (𝐽 ∈ Top →
((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽) | 
| 6 | 3, 5 | syl 17 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽) | 
| 7 |  | toponuni 22921 | . . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 8 | 7 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 = ∪ 𝐽) | 
| 9 | 8 | pweqd 4616 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝒫 𝑋 = 𝒫 ∪
𝐽) | 
| 10 | 6, 9 | sseqtrrd 4020 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋) | 
| 11 |  | toponmax 22933 | . . . . . . . . . 10
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) | 
| 12 |  | elpw2g 5332 | . . . . . . . . . 10
⊢ (𝑋 ∈ 𝐽 → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋)) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋)) | 
| 14 | 13 | biimpar 477 | . . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ 𝒫 𝑋) | 
| 15 | 14 | 3adant3 1132 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝒫 𝑋) | 
| 16 | 15 | snssd 4808 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ⊆ 𝒫 𝑋) | 
| 17 | 10, 16 | unssd 4191 | . . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋) | 
| 18 |  | ssun2 4178 | . . . . . 6
⊢ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) | 
| 19 | 11 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽) | 
| 20 |  | simp2 1137 | . . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋) | 
| 21 | 19, 20 | ssexd 5323 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V) | 
| 22 | 21 | snn0d 4774 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ≠ ∅) | 
| 23 |  | ssn0 4403 | . . . . . 6
⊢ (({𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∧ {𝑆} ≠ ∅) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅) | 
| 24 | 18, 22, 23 | sylancr 587 | . . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅) | 
| 25 | 20, 8 | sseqtrd 4019 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ ∪ 𝐽) | 
| 26 |  | simp3 1138 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆)) | 
| 27 | 4 | neindisj 23126 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ (𝐴 ∈
((cls‘𝐽)‘𝑆) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥 ∩ 𝑆) ≠ ∅) | 
| 28 | 27 | expr 456 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ 𝐴 ∈
((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥 ∩ 𝑆) ≠ ∅)) | 
| 29 | 3, 25, 26, 28 | syl21anc 837 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥 ∩ 𝑆) ≠ ∅)) | 
| 30 | 29 | imp 406 | . . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥 ∩ 𝑆) ≠ ∅) | 
| 31 |  | elsni 4642 | . . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑆} → 𝑦 = 𝑆) | 
| 32 | 31 | ineq2d 4219 | . . . . . . . . . 10
⊢ (𝑦 ∈ {𝑆} → (𝑥 ∩ 𝑦) = (𝑥 ∩ 𝑆)) | 
| 33 | 32 | neeq1d 2999 | . . . . . . . . 9
⊢ (𝑦 ∈ {𝑆} → ((𝑥 ∩ 𝑦) ≠ ∅ ↔ (𝑥 ∩ 𝑆) ≠ ∅)) | 
| 34 | 30, 33 | syl5ibrcom 247 | . . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑦 ∈ {𝑆} → (𝑥 ∩ 𝑦) ≠ ∅)) | 
| 35 | 34 | ralrimiv 3144 | . . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅) | 
| 36 | 35 | ralrimiva 3145 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅) | 
| 37 |  | simp1 1136 | . . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 38 | 4 | clsss3 23068 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽) | 
| 39 | 3, 25, 38 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽) | 
| 40 | 39, 26 | sseldd 3983 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ∪ 𝐽) | 
| 41 | 40, 8 | eleqtrrd 2843 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ 𝑋) | 
| 42 | 41 | snssd 4808 | . . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ⊆ 𝑋) | 
| 43 |  | snnzg 4773 | . . . . . . . . . 10
⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑆) → {𝐴} ≠ ∅) | 
| 44 | 43 | 3ad2ant3 1135 | . . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ≠ ∅) | 
| 45 |  | neifil 23889 | . . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋)) | 
| 46 | 37, 42, 44, 45 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋)) | 
| 47 |  | filfbas 23857 | . . . . . . . 8
⊢
(((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) | 
| 48 | 46, 47 | syl 17 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) | 
| 49 |  | ne0i 4340 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑆) → ((cls‘𝐽)‘𝑆) ≠ ∅) | 
| 50 | 49 | 3ad2ant3 1135 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ∅) | 
| 51 |  | cls0 23089 | . . . . . . . . . . 11
⊢ (𝐽 ∈ Top →
((cls‘𝐽)‘∅) = ∅) | 
| 52 | 3, 51 | syl 17 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘∅) = ∅) | 
| 53 | 50, 52 | neeqtrrd 3014 | . . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅)) | 
| 54 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑆 = ∅ →
((cls‘𝐽)‘𝑆) = ((cls‘𝐽)‘∅)) | 
| 55 | 54 | necon3i 2972 | . . . . . . . . 9
⊢
(((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅) → 𝑆 ≠ ∅) | 
| 56 | 53, 55 | syl 17 | . . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ≠ ∅) | 
| 57 |  | snfbas 23875 | . . . . . . . 8
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ∧ 𝑋 ∈ 𝐽) → {𝑆} ∈ (fBas‘𝑋)) | 
| 58 | 20, 56, 19, 57 | syl3anc 1372 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ∈ (fBas‘𝑋)) | 
| 59 |  | fbunfip 23878 | . . . . . . 7
⊢
((((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋) ∧ {𝑆} ∈ (fBas‘𝑋)) → (¬ ∅ ∈
(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅)) | 
| 60 | 48, 58, 59 | syl2anc 584 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ ∅ ∈
(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥 ∩ 𝑦) ≠ ∅)) | 
| 61 | 36, 60 | mpbird 257 | . . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ ∅ ∈
(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) | 
| 62 |  | fsubbas 23876 | . . . . . 6
⊢ (𝑋 ∈ 𝐽 → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))) | 
| 63 | 19, 62 | syl 17 | . . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))) | 
| 64 | 17, 24, 61, 63 | mpbir3and 1342 | . . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋)) | 
| 65 |  | fgcl 23887 | . . . 4
⊢
((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋)) | 
| 66 | 64, 65 | syl 17 | . . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋)) | 
| 67 | 1, 66 | eqeltrid 2844 | . 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐹 ∈ (Fil‘𝑋)) | 
| 68 |  | fvex 6918 | . . . . . 6
⊢
((nei‘𝐽)‘{𝐴}) ∈ V | 
| 69 |  | snex 5435 | . . . . . 6
⊢ {𝑆} ∈ V | 
| 70 | 68, 69 | unex 7765 | . . . . 5
⊢
(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V | 
| 71 |  | ssfii 9460 | . . . . 5
⊢
((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) | 
| 72 | 70, 71 | ax-mp 5 | . . . 4
⊢
(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) | 
| 73 |  | ssfg 23881 | . . . . . 6
⊢
((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))) | 
| 74 | 64, 73 | syl 17 | . . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))) | 
| 75 | 74, 1 | sseqtrrdi 4024 | . . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ 𝐹) | 
| 76 | 72, 75 | sstrid 3994 | . . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝐹) | 
| 77 |  | snssg 4782 | . . . . 5
⊢ (𝑆 ∈ V → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) | 
| 78 | 21, 77 | syl 17 | . . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) | 
| 79 | 18, 78 | mpbiri 258 | . . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) | 
| 80 | 76, 79 | sseldd 3983 | . 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐹) | 
| 81 | 76 | unssad 4192 | . . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹) | 
| 82 |  | elflim 23980 | . . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹))) | 
| 83 | 37, 67, 82 | syl2anc 584 | . . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹))) | 
| 84 | 41, 81, 83 | mpbir2and 713 | . 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ (𝐽 fLim 𝐹)) | 
| 85 | 67, 80, 84 | 3jca 1128 | 1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹))) |