Proof of Theorem cnextfvval
| Step | Hyp | Ref
| Expression |
| 1 | | cnextf.3 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Top) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐽 ∈ Top) |
| 3 | | cnextf.4 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ Haus) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐾 ∈ Haus) |
| 5 | | cnextf.5 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 6 | 5 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐹:𝐴⟶𝐵) |
| 7 | | cnextf.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| 8 | 7 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐴 ⊆ 𝐶) |
| 9 | | cnextf.1 |
. . . 4
⊢ 𝐶 = ∪
𝐽 |
| 10 | | cnextf.2 |
. . . 4
⊢ 𝐵 = ∪
𝐾 |
| 11 | 9, 10 | cnextfun 24072 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Haus) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Fun ((𝐽CnExt𝐾)‘𝐹)) |
| 12 | 2, 4, 6, 8, 11 | syl22anc 839 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → Fun ((𝐽CnExt𝐾)‘𝐹)) |
| 13 | | cnextf.6 |
. . . . . 6
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) |
| 14 | 13 | eleq2d 2827 |
. . . . 5
⊢ (𝜑 → (𝑋 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑋 ∈ 𝐶)) |
| 15 | 14 | biimpar 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ ((cls‘𝐽)‘𝐴)) |
| 16 | | fvex 6919 |
. . . . . . 7
⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ V |
| 17 | 16 | uniex 7761 |
. . . . . 6
⊢ ∪ ((𝐾
fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ V |
| 18 | 17 | snid 4662 |
. . . . 5
⊢ ∪ ((𝐾
fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ {∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)} |
| 19 | | sneq 4636 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
| 20 | 19 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑋})) |
| 21 | 20 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴)) |
| 22 | 21 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))) |
| 23 | 22 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |
| 24 | 23 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ≈ 1o)) |
| 25 | 24 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝜑 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o) ↔ (𝜑 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ≈ 1o))) |
| 26 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ Haus) |
| 27 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐽 ∈ Top) |
| 28 | 9 | toptopon 22923 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶)) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶)) |
| 30 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶) |
| 31 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
| 32 | 13 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥 ∈ 𝐶)) |
| 33 | 32 | biimpar 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴)) |
| 34 | | trnei 23900 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
| 35 | 34 | biimpa 476 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) ∧ 𝑥 ∈ ((cls‘𝐽)‘𝐴)) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)) |
| 36 | 29, 30, 31, 33, 35 | syl31anc 1375 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)) |
| 37 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:𝐴⟶𝐵) |
| 38 | | cnextf.7 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) |
| 39 | 10 | hausflf2 24006 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ Haus ∧
(((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o) |
| 40 | 26, 36, 37, 38, 39 | syl31anc 1375 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o) |
| 41 | 40 | expcom 413 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐶 → (𝜑 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o)) |
| 42 | 25, 41 | vtoclga 3577 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐶 → (𝜑 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ≈ 1o)) |
| 43 | 42 | impcom 407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ≈ 1o) |
| 44 | | en1b 9065 |
. . . . . 6
⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ≈ 1o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)}) |
| 45 | 43, 44 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)}) |
| 46 | 18, 45 | eleqtrrid 2848 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |
| 47 | | nfiu1 5027 |
. . . . . . . 8
⊢
Ⅎ𝑥∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) |
| 48 | 47 | nfel2 2924 |
. . . . . . 7
⊢
Ⅎ𝑥〈𝑋, ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) |
| 49 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑋 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |
| 50 | 48, 49 | nfbi 1903 |
. . . . . 6
⊢
Ⅎ𝑥(〈𝑋, ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑋 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
| 51 | | opeq1 4873 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → 〈𝑥, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 = 〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉) |
| 52 | 51 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (〈𝑥, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ 〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))) |
| 53 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑋 ∈ ((cls‘𝐽)‘𝐴))) |
| 54 | 23 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
| 55 | 53, 54 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑋 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)))) |
| 56 | 52, 55 | bibi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ((〈𝑥, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) ↔ (〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑋 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))))) |
| 57 | | opeliunxp 5752 |
. . . . . 6
⊢
(〈𝑥, ∪ ((𝐾
fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
| 58 | 50, 56, 57 | vtoclg1f 3570 |
. . . . 5
⊢ (𝑋 ∈ 𝐶 → (〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑋 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)))) |
| 59 | 58 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑋 ∈ ((cls‘𝐽)‘𝐴) ∧ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)))) |
| 60 | 15, 46, 59 | mpbir2and 713 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
| 61 | | df-br 5144 |
. . . 4
⊢ (𝑋((𝐽CnExt𝐾)‘𝐹)∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ↔ 〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ((𝐽CnExt𝐾)‘𝐹)) |
| 62 | | haustop 23339 |
. . . . . . . 8
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) |
| 63 | 3, 62 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
| 64 | 63 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐾 ∈ Top) |
| 65 | 9, 10 | cnextfval 24070 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → ((𝐽CnExt𝐾)‘𝐹) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
| 66 | 2, 64, 6, 8, 65 | syl22anc 839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐽CnExt𝐾)‘𝐹) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
| 67 | 66 | eleq2d 2827 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ((𝐽CnExt𝐾)‘𝐹) ↔ 〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))) |
| 68 | 61, 67 | bitrid 283 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑋((𝐽CnExt𝐾)‘𝐹)∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ↔ 〈𝑋, ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))) |
| 69 | 60, 68 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑋((𝐽CnExt𝐾)‘𝐹)∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |
| 70 | | funbrfv 6957 |
. 2
⊢ (Fun
((𝐽CnExt𝐾)‘𝐹) → (𝑋((𝐽CnExt𝐾)‘𝐹)∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
| 71 | 12, 69, 70 | sylc 65 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |