Step | Hyp | Ref
| Expression |
1 | | cnextfres.j |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
2 | | cnextfres.k |
. . 3
⊢ (𝜑 → 𝐾 ∈ Haus) |
3 | | cnextfres.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) |
4 | | eqid 2826 |
. . . . . 6
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) |
5 | | cnextfres.b |
. . . . . 6
⊢ 𝐵 = ∪
𝐾 |
6 | 4, 5 | cnf 21422 |
. . . . 5
⊢ (𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) → 𝐹:∪ (𝐽 ↾t 𝐴)⟶𝐵) |
7 | 3, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:∪ (𝐽 ↾t 𝐴)⟶𝐵) |
8 | | cnextfres.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
9 | | cnextfres.c |
. . . . . . 7
⊢ 𝐶 = ∪
𝐽 |
10 | 9 | restuni 21338 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
11 | 1, 8, 10 | syl2anc 581 |
. . . . 5
⊢ (𝜑 → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
12 | 11 | feq2d 6265 |
. . . 4
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:∪ (𝐽 ↾t 𝐴)⟶𝐵)) |
13 | 7, 12 | mpbird 249 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
14 | 9, 5 | cnextfun 22239 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Haus) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Fun ((𝐽CnExt𝐾)‘𝐹)) |
15 | 1, 2, 13, 8, 14 | syl22anc 874 |
. 2
⊢ (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹)) |
16 | 9 | sscls 21232 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ ((cls‘𝐽)‘𝐴)) |
17 | 1, 8, 16 | syl2anc 581 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ((cls‘𝐽)‘𝐴)) |
18 | | cnextfres.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
19 | 17, 18 | sseldd 3829 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ((cls‘𝐽)‘𝐴)) |
20 | 9, 5, 1, 8, 3, 18 | flfcntr 22218 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |
21 | 19, 20 | jca 509 |
. . . . 5
⊢ (𝜑 → (𝑋 ∈ ((cls‘𝐽)‘𝐴) ∧ (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
22 | | sneq 4408 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
23 | 22 | fveq2d 6438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑋})) |
24 | 23 | oveq1d 6921 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴)) |
25 | 24 | oveq2d 6922 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))) |
26 | 25 | fveq1d 6436 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |
27 | 26 | opeliunxp2 5494 |
. . . . 5
⊢
(〈𝑋, (𝐹‘𝑋)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑋 ∈ ((cls‘𝐽)‘𝐴) ∧ (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
28 | 21, 27 | sylibr 226 |
. . . 4
⊢ (𝜑 → 〈𝑋, (𝐹‘𝑋)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
29 | | haustop 21507 |
. . . . . . 7
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) |
30 | 2, 29 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Top) |
31 | 9, 5 | cnextfval 22237 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → ((𝐽CnExt𝐾)‘𝐹) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
32 | 1, 30, 13, 8, 31 | syl22anc 874 |
. . . . 5
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
33 | 32 | eleq2d 2893 |
. . . 4
⊢ (𝜑 → (〈𝑋, (𝐹‘𝑋)〉 ∈ ((𝐽CnExt𝐾)‘𝐹) ↔ 〈𝑋, (𝐹‘𝑋)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))) |
34 | 28, 33 | mpbird 249 |
. . 3
⊢ (𝜑 → 〈𝑋, (𝐹‘𝑋)〉 ∈ ((𝐽CnExt𝐾)‘𝐹)) |
35 | | df-br 4875 |
. . 3
⊢ (𝑋((𝐽CnExt𝐾)‘𝐹)(𝐹‘𝑋) ↔ 〈𝑋, (𝐹‘𝑋)〉 ∈ ((𝐽CnExt𝐾)‘𝐹)) |
36 | 34, 35 | sylibr 226 |
. 2
⊢ (𝜑 → 𝑋((𝐽CnExt𝐾)‘𝐹)(𝐹‘𝑋)) |
37 | | funbrfv 6481 |
. . 3
⊢ (Fun
((𝐽CnExt𝐾)‘𝐹) → (𝑋((𝐽CnExt𝐾)‘𝐹)(𝐹‘𝑋) → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋))) |
38 | 37 | imp 397 |
. 2
⊢ ((Fun
((𝐽CnExt𝐾)‘𝐹) ∧ 𝑋((𝐽CnExt𝐾)‘𝐹)(𝐹‘𝑋)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋)) |
39 | 15, 36, 38 | syl2anc 581 |
1
⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋)) |