Step | Hyp | Ref
| Expression |
1 | | anass 459 |
. 2
⊢ ((((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝐹 ⊆ 𝒫 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)) ↔ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil) ∧ (𝐹 ⊆
𝒫 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))) |
2 | | df-3an 1073 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋) ↔ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil) ∧ 𝐹 ⊆
𝒫 𝑋)) |
3 | 2 | anbi1i 602 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)) ↔ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil) ∧ 𝐹 ⊆
𝒫 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹))) |
4 | | df-flim 21962 |
. . . 4
⊢ fLim =
(𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)}) |
5 | 4 | elmpt2cl 7022 |
. . 3
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → (𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil)) |
6 | | flimval.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
7 | 6 | flimval 21986 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐽 fLim 𝐹) = {𝑥 ∈ 𝑋 ∣ (((nei‘𝐽)‘{𝑥}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋)}) |
8 | 7 | eleq2d 2836 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ (((nei‘𝐽)‘{𝑥}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋)})) |
9 | | sneq 4326 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴}) |
10 | 9 | fveq2d 6336 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝐴})) |
11 | 10 | sseq1d 3781 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (((nei‘𝐽)‘{𝑥}) ⊆ 𝐹 ↔ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)) |
12 | 11 | anbi1d 607 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((((nei‘𝐽)‘{𝑥}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋) ↔ (((nei‘𝐽)‘{𝐴}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋))) |
13 | | ancom 452 |
. . . . . . 7
⊢
((((nei‘𝐽)‘{𝐴}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)) |
14 | 12, 13 | syl6bb 276 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((((nei‘𝐽)‘{𝑥}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹))) |
15 | 14 | elrab 3515 |
. . . . 5
⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ (((nei‘𝐽)‘{𝑥}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋)} ↔ (𝐴 ∈ 𝑋 ∧ (𝐹 ⊆ 𝒫 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹))) |
16 | | an12 616 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ (𝐹 ⊆ 𝒫 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹))) |
17 | 15, 16 | bitri 264 |
. . . 4
⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ (((nei‘𝐽)‘{𝑥}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋)} ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹))) |
18 | 8, 17 | syl6bb 276 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))) |
19 | 5, 18 | biadan2 802 |
. 2
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil) ∧ (𝐹 ⊆
𝒫 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))) |
20 | 1, 3, 19 | 3bitr4ri 293 |
1
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil
∧ 𝐹 ⊆ 𝒫
𝑋) ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹))) |