| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cnextf.3 | . . . 4
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 2 |  | cnextf.4 | . . . 4
⊢ (𝜑 → 𝐾 ∈ Haus) | 
| 3 |  | cnextf.5 | . . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 4 |  | cnextf.a | . . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝐶) | 
| 5 |  | cnextf.1 | . . . . 5
⊢ 𝐶 = ∪
𝐽 | 
| 6 |  | cnextf.2 | . . . . 5
⊢ 𝐵 = ∪
𝐾 | 
| 7 | 5, 6 | cnextfun 24072 | . . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Haus) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Fun ((𝐽CnExt𝐾)‘𝐹)) | 
| 8 | 1, 2, 3, 4, 7 | syl22anc 839 | . . 3
⊢ (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹)) | 
| 9 |  | dfdm3 5898 | . . . 4
⊢ dom
((𝐽CnExt𝐾)‘𝐹) = {𝑥 ∣ ∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹)} | 
| 10 |  | simpl 482 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜑) | 
| 11 |  | cnextf.6 | . . . . . . . . 9
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) | 
| 12 | 11 | eleq2d 2827 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥 ∈ 𝐶)) | 
| 13 | 12 | biimpar 477 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴)) | 
| 14 |  | cnextf.7 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) | 
| 15 |  | n0 4353 | . . . . . . . 8
⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) | 
| 16 | 14, 15 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑦 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) | 
| 17 |  | haustop 23339 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) | 
| 18 | 2, 17 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 19 | 5, 6 | cnextfval 24070 | . . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → ((𝐽CnExt𝐾)‘𝐹) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) | 
| 20 | 1, 18, 3, 4, 19 | syl22anc 839 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) | 
| 21 | 20 | eleq2d 2827 | . . . . . . . . . . 11
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹) ↔ 〈𝑥, 𝑦〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))) | 
| 22 |  | opeliunxp 5752 | . . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) | 
| 23 | 21, 22 | bitrdi 287 | . . . . . . . . . 10
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹) ↔ (𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))) | 
| 24 | 23 | exbidv 1921 | . . . . . . . . 9
⊢ (𝜑 → (∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹) ↔ ∃𝑦(𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))) | 
| 25 |  | 19.42v 1953 | . . . . . . . . 9
⊢
(∃𝑦(𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ↔ (𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ ∃𝑦 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) | 
| 26 | 24, 25 | bitrdi 287 | . . . . . . . 8
⊢ (𝜑 → (∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹) ↔ (𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ ∃𝑦 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))) | 
| 27 | 26 | biimpar 477 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((cls‘𝐽)‘𝐴) ∧ ∃𝑦 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) → ∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹)) | 
| 28 | 10, 13, 16, 27 | syl12anc 837 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹)) | 
| 29 | 26 | simprbda 498 | . . . . . . 7
⊢ ((𝜑 ∧ ∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹)) → 𝑥 ∈ ((cls‘𝐽)‘𝐴)) | 
| 30 | 12 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹)) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥 ∈ 𝐶)) | 
| 31 | 29, 30 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ ∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹)) → 𝑥 ∈ 𝐶) | 
| 32 | 28, 31 | impbida 801 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹))) | 
| 33 | 32 | eqabdv 2875 | . . . 4
⊢ (𝜑 → 𝐶 = {𝑥 ∣ ∃𝑦〈𝑥, 𝑦〉 ∈ ((𝐽CnExt𝐾)‘𝐹)}) | 
| 34 | 9, 33 | eqtr4id 2796 | . . 3
⊢ (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶) | 
| 35 |  | df-fn 6564 | . . 3
⊢ (((𝐽CnExt𝐾)‘𝐹) Fn 𝐶 ↔ (Fun ((𝐽CnExt𝐾)‘𝐹) ∧ dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)) | 
| 36 | 8, 34, 35 | sylanbrc 583 | . 2
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) Fn 𝐶) | 
| 37 | 20 | rneqd 5949 | . . 3
⊢ (𝜑 → ran ((𝐽CnExt𝐾)‘𝐹) = ran ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) | 
| 38 |  | rniun 6167 | . . . 4
⊢ ran
∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)ran ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) | 
| 39 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 40 | 39 | snnz 4776 | . . . . . . . 8
⊢ {𝑥} ≠ ∅ | 
| 41 |  | rnxp 6190 | . . . . . . . 8
⊢ ({𝑥} ≠ ∅ → ran
({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) | 
| 42 | 40, 41 | ax-mp 5 | . . . . . . 7
⊢ ran
({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) | 
| 43 | 12 | biimpa 476 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((cls‘𝐽)‘𝐴)) → 𝑥 ∈ 𝐶) | 
| 44 | 6 | toptopon 22923 | . . . . . . . . . . 11
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵)) | 
| 45 | 18, 44 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐵)) | 
| 46 | 45 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵)) | 
| 47 | 5 | toptopon 22923 | . . . . . . . . . . . 12
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶)) | 
| 48 | 1, 47 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶)) | 
| 49 | 48 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶)) | 
| 50 | 4 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶) | 
| 51 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) | 
| 52 |  | trnei 23900 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))) | 
| 53 | 52 | biimpa 476 | . . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) ∧ 𝑥 ∈ ((cls‘𝐽)‘𝐴)) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)) | 
| 54 | 49, 50, 51, 13, 53 | syl31anc 1375 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)) | 
| 55 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:𝐴⟶𝐵) | 
| 56 |  | flfelbas 24002 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) → 𝑦 ∈ 𝐵) | 
| 57 | 56 | ex 412 | . . . . . . . . . 10
⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → (𝑦 ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) → 𝑦 ∈ 𝐵)) | 
| 58 | 57 | ssrdv 3989 | . . . . . . . . 9
⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ⊆ 𝐵) | 
| 59 | 46, 54, 55, 58 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ⊆ 𝐵) | 
| 60 | 43, 59 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((cls‘𝐽)‘𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ⊆ 𝐵) | 
| 61 | 42, 60 | eqsstrid 4022 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((cls‘𝐽)‘𝐴)) → ran ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ⊆ 𝐵) | 
| 62 | 61 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ((cls‘𝐽)‘𝐴)ran ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ⊆ 𝐵) | 
| 63 |  | iunss 5045 | . . . . 5
⊢ (∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)ran ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ⊆ 𝐵 ↔ ∀𝑥 ∈ ((cls‘𝐽)‘𝐴)ran ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ⊆ 𝐵) | 
| 64 | 62, 63 | sylibr 234 | . . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)ran ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ⊆ 𝐵) | 
| 65 | 38, 64 | eqsstrid 4022 | . . 3
⊢ (𝜑 → ran ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ⊆ 𝐵) | 
| 66 | 37, 65 | eqsstrd 4018 | . 2
⊢ (𝜑 → ran ((𝐽CnExt𝐾)‘𝐹) ⊆ 𝐵) | 
| 67 |  | df-f 6565 | . 2
⊢ (((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵 ↔ (((𝐽CnExt𝐾)‘𝐹) Fn 𝐶 ∧ ran ((𝐽CnExt𝐾)‘𝐹) ⊆ 𝐵)) | 
| 68 | 36, 66, 67 | sylanbrc 583 | 1
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) |