| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fbflim.3 | . . 3
⊢ 𝐹 = (𝑋filGen𝐵) | 
| 2 | 1 | fbflim 23985 | . 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦)))) | 
| 3 |  | topontop 22920 | . . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | 
| 4 | 3 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ Top) | 
| 5 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋) | 
| 6 |  | toponuni 22921 | . . . . . . . . . 10
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 7 | 6 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → 𝑋 = ∪ 𝐽) | 
| 8 | 5, 7 | eleqtrd 2842 | . . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ ∪ 𝐽) | 
| 9 |  | eqid 2736 | . . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 10 | 9 | isneip 23114 | . . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ∪ 𝐽)
→ (𝑛 ∈
((nei‘𝐽)‘{𝐴}) ↔ (𝑛 ⊆ ∪ 𝐽 ∧ ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)))) | 
| 11 | 4, 8, 10 | syl2anc 584 | . . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → (𝑛 ∈ ((nei‘𝐽)‘{𝐴}) ↔ (𝑛 ⊆ ∪ 𝐽 ∧ ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)))) | 
| 12 |  | simpr 484 | . . . . . . 7
⊢ ((𝑛 ⊆ ∪ 𝐽
∧ ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)) → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)) | 
| 13 | 11, 12 | biimtrdi 253 | . . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → (𝑛 ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛))) | 
| 14 |  | r19.29 3113 | . . . . . . . 8
⊢
((∀𝑦 ∈
𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) ∧ ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)) → ∃𝑦 ∈ 𝐽 ((𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) ∧ (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛))) | 
| 15 |  | pm3.45 622 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) → ((𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛) → (∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑛))) | 
| 16 | 15 | imp 406 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) ∧ (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)) → (∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑛)) | 
| 17 |  | sstr2 3989 | . . . . . . . . . . . . 13
⊢ (𝑥 ⊆ 𝑦 → (𝑦 ⊆ 𝑛 → 𝑥 ⊆ 𝑛)) | 
| 18 | 17 | com12 32 | . . . . . . . . . . . 12
⊢ (𝑦 ⊆ 𝑛 → (𝑥 ⊆ 𝑦 → 𝑥 ⊆ 𝑛)) | 
| 19 | 18 | reximdv 3169 | . . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝑛 → (∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛)) | 
| 20 | 19 | impcom 407 | . . . . . . . . . 10
⊢
((∃𝑥 ∈
𝐵 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑛) → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛) | 
| 21 | 16, 20 | syl 17 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) ∧ (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)) → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛) | 
| 22 | 21 | rexlimivw 3150 | . . . . . . . 8
⊢
(∃𝑦 ∈
𝐽 ((𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) ∧ (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)) → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛) | 
| 23 | 14, 22 | syl 17 | . . . . . . 7
⊢
((∀𝑦 ∈
𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) ∧ ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛)) → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛) | 
| 24 | 23 | ex 412 | . . . . . 6
⊢
(∀𝑦 ∈
𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) → (∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛) → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛)) | 
| 25 | 13, 24 | syl9 77 | . . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) → (𝑛 ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛))) | 
| 26 | 25 | ralrimdv 3151 | . . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) → ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛)) | 
| 27 | 4 | adantr 480 | . . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦)) → 𝐽 ∈ Top) | 
| 28 |  | simprl 770 | . . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦)) → 𝑦 ∈ 𝐽) | 
| 29 |  | simprr 772 | . . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦)) → 𝐴 ∈ 𝑦) | 
| 30 |  | opnneip 23128 | . . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦) → 𝑦 ∈ ((nei‘𝐽)‘{𝐴})) | 
| 31 | 27, 28, 29, 30 | syl3anc 1372 | . . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦)) → 𝑦 ∈ ((nei‘𝐽)‘{𝐴})) | 
| 32 |  | sseq2 4009 | . . . . . . . . . 10
⊢ (𝑛 = 𝑦 → (𝑥 ⊆ 𝑛 ↔ 𝑥 ⊆ 𝑦)) | 
| 33 | 32 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑛 = 𝑦 → (∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ↔ ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦)) | 
| 34 | 33 | rspcv 3617 | . . . . . . . 8
⊢ (𝑦 ∈ ((nei‘𝐽)‘{𝐴}) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦)) | 
| 35 | 31, 34 | syl 17 | . . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦)) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦)) | 
| 36 | 35 | expr 456 | . . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦))) | 
| 37 | 36 | com23 86 | . . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝐽) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦))) | 
| 38 | 37 | ralrimdva 3153 | . . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦))) | 
| 39 | 26, 38 | impbid 212 | . . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛)) | 
| 40 | 39 | pm5.32da 579 | . 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → ((𝐴 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦)) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛))) | 
| 41 | 2, 40 | bitrd 279 | 1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛))) |