| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cnextf.1 | . . . . 5
⊢ 𝐶 = ∪
𝐽 | 
| 2 |  | cnextf.2 | . . . . 5
⊢ 𝐵 = ∪
𝐾 | 
| 3 |  | cnextf.3 | . . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 4 |  | cnextf.4 | . . . . 5
⊢ (𝜑 → 𝐾 ∈ Haus) | 
| 5 |  | cnextf.5 | . . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 6 |  | cnextf.a | . . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝐶) | 
| 7 |  | cnextf.6 | . . . . 5
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) | 
| 8 |  | cnextf.7 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) | 
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | cnextf 24075 | . . . 4
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) | 
| 10 | 9 | ffnd 6736 | . . 3
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) Fn 𝐶) | 
| 11 |  | fnssres 6690 | . . 3
⊢ ((((𝐽CnExt𝐾)‘𝐹) Fn 𝐶 ∧ 𝐴 ⊆ 𝐶) → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) Fn 𝐴) | 
| 12 | 10, 6, 11 | syl2anc 584 | . 2
⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) Fn 𝐴) | 
| 13 | 5 | ffnd 6736 | . 2
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 14 |  | fvres 6924 | . . . 4
⊢ (𝑦 ∈ 𝐴 → ((((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴)‘𝑦) = (((𝐽CnExt𝐾)‘𝐹)‘𝑦)) | 
| 15 | 14 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴)‘𝑦) = (((𝐽CnExt𝐾)‘𝐹)‘𝑦)) | 
| 16 | 6 | sselda 3982 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐶) | 
| 17 | 1, 2, 3, 4, 5, 6, 7, 8 | cnextfvval 24074 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑦) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) | 
| 18 | 16, 17 | syldan 591 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝐽CnExt𝐾)‘𝐹)‘𝑦) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) | 
| 19 | 5 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐵) | 
| 20 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) | 
| 21 | 1 | restuni 23171 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | 
| 22 | 3, 6, 21 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | 
| 24 | 20, 23 | eleqtrd 2842 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ∪ (𝐽 ↾t 𝐴)) | 
| 25 |  | cnextfres1.1 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) | 
| 26 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢
((cls‘𝐽)‘𝐴) ∈ V | 
| 27 | 7, 26 | eqeltrrdi 2849 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ V) | 
| 28 | 27, 6 | ssexd 5323 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ V) | 
| 29 |  | resttop 23169 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top) | 
| 30 | 3, 28, 29 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Top) | 
| 31 |  | haustop 23340 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) | 
| 32 | 4, 31 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 33 | 22 | feq2d 6721 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:∪ (𝐽 ↾t 𝐴)⟶𝐵)) | 
| 34 | 5, 33 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:∪ (𝐽 ↾t 𝐴)⟶𝐵) | 
| 35 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) | 
| 36 | 35, 2 | cnnei 23291 | . . . . . . . . . . . . . 14
⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:∪
(𝐽 ↾t
𝐴)⟶𝐵) → (𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ ∀𝑦 ∈ ∪ (𝐽 ↾t 𝐴)∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤)) | 
| 37 | 30, 32, 34, 36 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ ∀𝑦 ∈ ∪ (𝐽 ↾t 𝐴)∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤)) | 
| 38 | 25, 37 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ ∪ (𝐽 ↾t 𝐴)∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤) | 
| 39 | 38 | r19.21bi 3250 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ (𝐽 ↾t 𝐴)) → ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤) | 
| 40 | 24, 39 | syldan 591 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤) | 
| 41 | 40 | r19.21bi 3250 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})) → ∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤) | 
| 42 |  | snssi 4807 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐴 → {𝑦} ⊆ 𝐴) | 
| 43 | 1 | neitr 23189 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ∧ {𝑦} ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)) | 
| 44 | 3, 6, 42, 43 | syl2an3an 1423 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)) | 
| 45 | 44 | rexeqdv 3326 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤 ↔ ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤)) | 
| 46 | 45 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})) → (∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤 ↔ ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤)) | 
| 47 | 41, 46 | mpbid 232 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})) → ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤) | 
| 48 | 47 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤) | 
| 49 | 4 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Haus) | 
| 50 | 2 | toptopon 22924 | . . . . . . . . . 10
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵)) | 
| 51 | 50 | biimpi 216 | . . . . . . . . 9
⊢ (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘𝐵)) | 
| 52 | 49, 31, 51 | 3syl 18 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ (TopOn‘𝐵)) | 
| 53 | 7 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((cls‘𝐽)‘𝐴) = 𝐶) | 
| 54 | 16, 53 | eleqtrrd 2843 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ((cls‘𝐽)‘𝐴)) | 
| 55 | 1 | toptopon 22924 | . . . . . . . . . . . 12
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶)) | 
| 56 | 3, 55 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶)) | 
| 57 | 56 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐶)) | 
| 58 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 ⊆ 𝐶) | 
| 59 |  | trnei 23901 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑦 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴))) | 
| 60 | 57, 58, 16, 59 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴))) | 
| 61 | 54, 60 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴)) | 
| 62 | 5 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐹:𝐴⟶𝐵) | 
| 63 |  | flfnei 24000 | . . . . . . . 8
⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((𝐹‘𝑦) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ↔ ((𝐹‘𝑦) ∈ 𝐵 ∧ ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤))) | 
| 64 | 52, 61, 62, 63 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ↔ ((𝐹‘𝑦) ∈ 𝐵 ∧ ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤))) | 
| 65 | 19, 48, 64 | mpbir2and 713 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) | 
| 66 |  | eleq1w 2823 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶)) | 
| 67 | 66 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑦 ∈ 𝐶))) | 
| 68 |  | sneq 4635 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) | 
| 69 | 68 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦})) | 
| 70 | 69 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)) | 
| 71 | 70 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))) | 
| 72 | 71 | fveq1d 6907 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) | 
| 73 | 72 | neeq1d 2999 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)) | 
| 74 | 67, 73 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))) | 
| 75 | 74, 8 | chvarvv 1997 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅) | 
| 76 | 16, 75 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅) | 
| 77 | 2 | hausflf2 24007 | . . . . . . 7
⊢ (((𝐾 ∈ Haus ∧
(((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≈ 1o) | 
| 78 | 49, 61, 62, 76, 77 | syl31anc 1374 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≈ 1o) | 
| 79 |  | en1eqsn 9309 | . . . . . 6
⊢ (((𝐹‘𝑦) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≈ 1o) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) = {(𝐹‘𝑦)}) | 
| 80 | 65, 78, 79 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) = {(𝐹‘𝑦)}) | 
| 81 | 80 | unieqd 4919 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) = ∪ {(𝐹‘𝑦)}) | 
| 82 |  | fvex 6918 | . . . . 5
⊢ (𝐹‘𝑦) ∈ V | 
| 83 | 82 | unisn 4925 | . . . 4
⊢ ∪ {(𝐹‘𝑦)} = (𝐹‘𝑦) | 
| 84 | 81, 83 | eqtrdi 2792 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) = (𝐹‘𝑦)) | 
| 85 | 15, 18, 84 | 3eqtrd 2780 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) | 
| 86 | 12, 13, 85 | eqfnfvd 7053 | 1
⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) = 𝐹) |