| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | kgencn 23564 | . 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ ((𝑘Gen‘𝐽) Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))))) | 
| 2 |  | rncmp 23404 | . . . . . . . 8
⊢ ((𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽)) → (𝐽 ↾t ran 𝑔) ∈ Comp) | 
| 3 | 2 | adantl 481 | . . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → (𝐽 ↾t ran 𝑔) ∈ Comp) | 
| 4 |  | simprr 773 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → 𝑔 ∈ (𝑧 Cn 𝐽)) | 
| 5 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ ∪ 𝑧 =
∪ 𝑧 | 
| 6 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 7 | 5, 6 | cnf 23254 | . . . . . . . . . . 11
⊢ (𝑔 ∈ (𝑧 Cn 𝐽) → 𝑔:∪ 𝑧⟶∪ 𝐽) | 
| 8 |  | frn 6743 | . . . . . . . . . . 11
⊢ (𝑔:∪
𝑧⟶∪ 𝐽
→ ran 𝑔 ⊆ ∪ 𝐽) | 
| 9 | 4, 7, 8 | 3syl 18 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → ran 𝑔 ⊆ ∪ 𝐽) | 
| 10 |  | toponuni 22920 | . . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 11 | 10 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → 𝑋 = ∪ 𝐽) | 
| 12 | 9, 11 | sseqtrrd 4021 | . . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → ran 𝑔 ⊆ 𝑋) | 
| 13 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑔 ∈ V | 
| 14 | 13 | rnex 7932 | . . . . . . . . . 10
⊢ ran 𝑔 ∈ V | 
| 15 | 14 | elpw 4604 | . . . . . . . . 9
⊢ (ran
𝑔 ∈ 𝒫 𝑋 ↔ ran 𝑔 ⊆ 𝑋) | 
| 16 | 12, 15 | sylibr 234 | . . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → ran 𝑔 ∈ 𝒫 𝑋) | 
| 17 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑘 = ran 𝑔 → (𝐽 ↾t 𝑘) = (𝐽 ↾t ran 𝑔)) | 
| 18 | 17 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑘 = ran 𝑔 → ((𝐽 ↾t 𝑘) ∈ Comp ↔ (𝐽 ↾t ran 𝑔) ∈ Comp)) | 
| 19 |  | reseq2 5992 | . . . . . . . . . . 11
⊢ (𝑘 = ran 𝑔 → (𝐹 ↾ 𝑘) = (𝐹 ↾ ran 𝑔)) | 
| 20 | 17 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝑘 = ran 𝑔 → ((𝐽 ↾t 𝑘) Cn 𝐾) = ((𝐽 ↾t ran 𝑔) Cn 𝐾)) | 
| 21 | 19, 20 | eleq12d 2835 | . . . . . . . . . 10
⊢ (𝑘 = ran 𝑔 → ((𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾) ↔ (𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾))) | 
| 22 | 18, 21 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑘 = ran 𝑔 → (((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)) ↔ ((𝐽 ↾t ran 𝑔) ∈ Comp → (𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾)))) | 
| 23 | 22 | rspcv 3618 | . . . . . . . 8
⊢ (ran
𝑔 ∈ 𝒫 𝑋 → (∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)) → ((𝐽 ↾t ran 𝑔) ∈ Comp → (𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾)))) | 
| 24 | 16, 23 | syl 17 | . . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → (∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)) → ((𝐽 ↾t ran 𝑔) ∈ Comp → (𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾)))) | 
| 25 | 3, 24 | mpid 44 | . . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → (∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)) → (𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾))) | 
| 26 |  | simplll 775 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 27 |  | ssidd 4007 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → ran 𝑔 ⊆ ran 𝑔) | 
| 28 |  | cnrest2 23294 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ran 𝑔 ⊆ ran 𝑔 ∧ ran 𝑔 ⊆ 𝑋) → (𝑔 ∈ (𝑧 Cn 𝐽) ↔ 𝑔 ∈ (𝑧 Cn (𝐽 ↾t ran 𝑔)))) | 
| 29 | 26, 27, 12, 28 | syl3anc 1373 | . . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → (𝑔 ∈ (𝑧 Cn 𝐽) ↔ 𝑔 ∈ (𝑧 Cn (𝐽 ↾t ran 𝑔)))) | 
| 30 | 4, 29 | mpbid 232 | . . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → 𝑔 ∈ (𝑧 Cn (𝐽 ↾t ran 𝑔))) | 
| 31 |  | cnco 23274 | . . . . . . . . 9
⊢ ((𝑔 ∈ (𝑧 Cn (𝐽 ↾t ran 𝑔)) ∧ (𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾)) → ((𝐹 ↾ ran 𝑔) ∘ 𝑔) ∈ (𝑧 Cn 𝐾)) | 
| 32 | 31 | ex 412 | . . . . . . . 8
⊢ (𝑔 ∈ (𝑧 Cn (𝐽 ↾t ran 𝑔)) → ((𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾) → ((𝐹 ↾ ran 𝑔) ∘ 𝑔) ∈ (𝑧 Cn 𝐾))) | 
| 33 | 30, 32 | syl 17 | . . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → ((𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾) → ((𝐹 ↾ ran 𝑔) ∘ 𝑔) ∈ (𝑧 Cn 𝐾))) | 
| 34 |  | ssid 4006 | . . . . . . . . 9
⊢ ran 𝑔 ⊆ ran 𝑔 | 
| 35 |  | cores 6269 | . . . . . . . . 9
⊢ (ran
𝑔 ⊆ ran 𝑔 → ((𝐹 ↾ ran 𝑔) ∘ 𝑔) = (𝐹 ∘ 𝑔)) | 
| 36 | 34, 35 | ax-mp 5 | . . . . . . . 8
⊢ ((𝐹 ↾ ran 𝑔) ∘ 𝑔) = (𝐹 ∘ 𝑔) | 
| 37 | 36 | eleq1i 2832 | . . . . . . 7
⊢ (((𝐹 ↾ ran 𝑔) ∘ 𝑔) ∈ (𝑧 Cn 𝐾) ↔ (𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾)) | 
| 38 | 33, 37 | imbitrdi 251 | . . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → ((𝐹 ↾ ran 𝑔) ∈ ((𝐽 ↾t ran 𝑔) Cn 𝐾) → (𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾))) | 
| 39 | 25, 38 | syld 47 | . . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ Comp ∧ 𝑔 ∈ (𝑧 Cn 𝐽))) → (∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)) → (𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾))) | 
| 40 | 39 | ralrimdvva 3211 | . . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)) → ∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾))) | 
| 41 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑧 = (𝐽 ↾t 𝑘) → (𝑧 Cn 𝐽) = ((𝐽 ↾t 𝑘) Cn 𝐽)) | 
| 42 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑧 = (𝐽 ↾t 𝑘) → (𝑧 Cn 𝐾) = ((𝐽 ↾t 𝑘) Cn 𝐾)) | 
| 43 | 42 | eleq2d 2827 | . . . . . . . . 9
⊢ (𝑧 = (𝐽 ↾t 𝑘) → ((𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾) ↔ (𝐹 ∘ 𝑔) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))) | 
| 44 | 41, 43 | raleqbidv 3346 | . . . . . . . 8
⊢ (𝑧 = (𝐽 ↾t 𝑘) → (∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾) ↔ ∀𝑔 ∈ ((𝐽 ↾t 𝑘) Cn 𝐽)(𝐹 ∘ 𝑔) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))) | 
| 45 | 44 | rspcv 3618 | . . . . . . 7
⊢ ((𝐽 ↾t 𝑘) ∈ Comp →
(∀𝑧 ∈ Comp
∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾) → ∀𝑔 ∈ ((𝐽 ↾t 𝑘) Cn 𝐽)(𝐹 ∘ 𝑔) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))) | 
| 46 |  | elpwi 4607 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝒫 𝑋 → 𝑘 ⊆ 𝑋) | 
| 47 | 46 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → 𝑘 ⊆ 𝑋) | 
| 48 | 47 | resabs1d 6026 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → (( I ↾ 𝑋) ↾ 𝑘) = ( I ↾ 𝑘)) | 
| 49 |  | idcn 23265 | . . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽 Cn 𝐽)) | 
| 50 | 49 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → ( I ↾ 𝑋) ∈ (𝐽 Cn 𝐽)) | 
| 51 | 10 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → 𝑋 = ∪ 𝐽) | 
| 52 | 47, 51 | sseqtrd 4020 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → 𝑘 ⊆ ∪ 𝐽) | 
| 53 | 6 | cnrest 23293 | . . . . . . . . . . 11
⊢ ((( I
↾ 𝑋) ∈ (𝐽 Cn 𝐽) ∧ 𝑘 ⊆ ∪ 𝐽) → (( I ↾ 𝑋) ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐽)) | 
| 54 | 50, 52, 53 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → (( I ↾ 𝑋) ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐽)) | 
| 55 | 48, 54 | eqeltrrd 2842 | . . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → ( I ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐽)) | 
| 56 |  | coeq2 5869 | . . . . . . . . . . 11
⊢ (𝑔 = ( I ↾ 𝑘) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ( I ↾ 𝑘))) | 
| 57 | 56 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑔 = ( I ↾ 𝑘) → ((𝐹 ∘ 𝑔) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾) ↔ (𝐹 ∘ ( I ↾ 𝑘)) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))) | 
| 58 | 57 | rspcv 3618 | . . . . . . . . 9
⊢ (( I
↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐽) → (∀𝑔 ∈ ((𝐽 ↾t 𝑘) Cn 𝐽)(𝐹 ∘ 𝑔) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾) → (𝐹 ∘ ( I ↾ 𝑘)) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))) | 
| 59 | 55, 58 | syl 17 | . . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → (∀𝑔 ∈ ((𝐽 ↾t 𝑘) Cn 𝐽)(𝐹 ∘ 𝑔) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾) → (𝐹 ∘ ( I ↾ 𝑘)) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))) | 
| 60 |  | coires1 6284 | . . . . . . . . 9
⊢ (𝐹 ∘ ( I ↾ 𝑘)) = (𝐹 ↾ 𝑘) | 
| 61 | 60 | eleq1i 2832 | . . . . . . . 8
⊢ ((𝐹 ∘ ( I ↾ 𝑘)) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾) ↔ (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)) | 
| 62 | 59, 61 | imbitrdi 251 | . . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → (∀𝑔 ∈ ((𝐽 ↾t 𝑘) Cn 𝐽)(𝐹 ∘ 𝑔) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾) → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))) | 
| 63 | 45, 62 | syl9r 78 | . . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → ((𝐽 ↾t 𝑘) ∈ Comp → (∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾) → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)))) | 
| 64 | 63 | com23 86 | . . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑘 ∈ 𝒫 𝑋) → (∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾) → ((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)))) | 
| 65 | 64 | ralrimdva 3154 | . . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾) → ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)))) | 
| 66 | 40, 65 | impbid 212 | . . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)) ↔ ∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾))) | 
| 67 | 66 | pm5.32da 579 | . 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾)))) | 
| 68 | 1, 67 | bitrd 279 | 1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ ((𝑘Gen‘𝐽) Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾)))) |