| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → 𝑔 ∈ (𝑅 Cn 𝑆)) |
| 2 | | xkoco2cn.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑆 Cn 𝑇)) |
| 3 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → 𝐹 ∈ (𝑆 Cn 𝑇)) |
| 4 | | cnco 23274 |
. . . 4
⊢ ((𝑔 ∈ (𝑅 Cn 𝑆) ∧ 𝐹 ∈ (𝑆 Cn 𝑇)) → (𝐹 ∘ 𝑔) ∈ (𝑅 Cn 𝑇)) |
| 5 | 1, 3, 4 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝐹 ∘ 𝑔) ∈ (𝑅 Cn 𝑇)) |
| 6 | 5 | fmpttd 7135 |
. 2
⊢ (𝜑 → (𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)):(𝑅 Cn 𝑆)⟶(𝑅 Cn 𝑇)) |
| 7 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑅 =
∪ 𝑅 |
| 8 | | eqid 2737 |
. . . . . 6
⊢ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp} = {𝑦 ∈
𝒫 ∪ 𝑅 ∣ (𝑅 ↾t 𝑦) ∈ Comp} |
| 9 | | eqid 2737 |
. . . . . 6
⊢ (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) |
| 10 | 7, 8, 9 | xkobval 23594 |
. . . . 5
⊢ ran
(𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ 𝒫 ∪ 𝑅∃𝑣 ∈ 𝑇 ((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})} |
| 11 | 10 | eqabri 2885 |
. . . 4
⊢ (𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ↔ ∃𝑘 ∈ 𝒫 ∪ 𝑅∃𝑣 ∈ 𝑇 ((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})) |
| 12 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → 𝑔 ∈ (𝑅 Cn 𝑆)) |
| 13 | 2 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → 𝐹 ∈ (𝑆 Cn 𝑇)) |
| 14 | 12, 13, 4 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝐹 ∘ 𝑔) ∈ (𝑅 Cn 𝑇)) |
| 15 | | imaeq1 6073 |
. . . . . . . . . . . . . 14
⊢ (ℎ = (𝐹 ∘ 𝑔) → (ℎ “ 𝑘) = ((𝐹 ∘ 𝑔) “ 𝑘)) |
| 16 | | imaco 6271 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∘ 𝑔) “ 𝑘) = (𝐹 “ (𝑔 “ 𝑘)) |
| 17 | 15, 16 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (ℎ = (𝐹 ∘ 𝑔) → (ℎ “ 𝑘) = (𝐹 “ (𝑔 “ 𝑘))) |
| 18 | 17 | sseq1d 4015 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝐹 ∘ 𝑔) → ((ℎ “ 𝑘) ⊆ 𝑣 ↔ (𝐹 “ (𝑔 “ 𝑘)) ⊆ 𝑣)) |
| 19 | 18 | elrab3 3693 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝑔) ∈ (𝑅 Cn 𝑇) → ((𝐹 ∘ 𝑔) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} ↔ (𝐹 “ (𝑔 “ 𝑘)) ⊆ 𝑣)) |
| 20 | 14, 19 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → ((𝐹 ∘ 𝑔) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} ↔ (𝐹 “ (𝑔 “ 𝑘)) ⊆ 𝑣)) |
| 21 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑆 =
∪ 𝑆 |
| 22 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑇 =
∪ 𝑇 |
| 23 | 21, 22 | cnf 23254 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (𝑆 Cn 𝑇) → 𝐹:∪ 𝑆⟶∪ 𝑇) |
| 24 | 2, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:∪ 𝑆⟶∪ 𝑇) |
| 25 | 24 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → 𝐹:∪ 𝑆⟶∪ 𝑇) |
| 26 | 25 | ffund 6740 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → Fun 𝐹) |
| 27 | | imassrn 6089 |
. . . . . . . . . . . . 13
⊢ (𝑔 “ 𝑘) ⊆ ran 𝑔 |
| 28 | 7, 21 | cnf 23254 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝑅 Cn 𝑆) → 𝑔:∪ 𝑅⟶∪ 𝑆) |
| 29 | 12, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → 𝑔:∪ 𝑅⟶∪ 𝑆) |
| 30 | 29 | frnd 6744 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → ran 𝑔 ⊆ ∪ 𝑆) |
| 31 | 27, 30 | sstrid 3995 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝑔 “ 𝑘) ⊆ ∪ 𝑆) |
| 32 | 25 | fdmd 6746 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → dom 𝐹 = ∪ 𝑆) |
| 33 | 31, 32 | sseqtrrd 4021 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝑔 “ 𝑘) ⊆ dom 𝐹) |
| 34 | | funimass3 7074 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ (𝑔 “ 𝑘) ⊆ dom 𝐹) → ((𝐹 “ (𝑔 “ 𝑘)) ⊆ 𝑣 ↔ (𝑔 “ 𝑘) ⊆ (◡𝐹 “ 𝑣))) |
| 35 | 26, 33, 34 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → ((𝐹 “ (𝑔 “ 𝑘)) ⊆ 𝑣 ↔ (𝑔 “ 𝑘) ⊆ (◡𝐹 “ 𝑣))) |
| 36 | 20, 35 | bitrd 279 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → ((𝐹 ∘ 𝑔) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} ↔ (𝑔 “ 𝑘) ⊆ (◡𝐹 “ 𝑣))) |
| 37 | 36 | rabbidva 3443 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → {𝑔 ∈ (𝑅 Cn 𝑆) ∣ (𝐹 ∘ 𝑔) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}} = {𝑔 ∈ (𝑅 Cn 𝑆) ∣ (𝑔 “ 𝑘) ⊆ (◡𝐹 “ 𝑣)}) |
| 38 | | xkoco2cn.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Top) |
| 39 | 38 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑅 ∈ Top) |
| 40 | | cntop1 23248 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 Cn 𝑇) → 𝑆 ∈ Top) |
| 41 | 2, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ Top) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑆 ∈ Top) |
| 43 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑘 ∈ 𝒫 ∪ 𝑅) |
| 44 | 43 | elpwid 4609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑘 ⊆ ∪ 𝑅) |
| 45 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → (𝑅 ↾t 𝑘) ∈ Comp) |
| 46 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝐹 ∈ (𝑆 Cn 𝑇)) |
| 47 | | simplrr 778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → 𝑣 ∈ 𝑇) |
| 48 | | cnima 23273 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ 𝑇) → (◡𝐹 “ 𝑣) ∈ 𝑆) |
| 49 | 46, 47, 48 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → (◡𝐹 “ 𝑣) ∈ 𝑆) |
| 50 | 7, 39, 42, 44, 45, 49 | xkoopn 23597 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → {𝑔 ∈ (𝑅 Cn 𝑆) ∣ (𝑔 “ 𝑘) ⊆ (◡𝐹 “ 𝑣)} ∈ (𝑆 ↑ko 𝑅)) |
| 51 | 37, 50 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → {𝑔 ∈ (𝑅 Cn 𝑆) ∣ (𝐹 ∘ 𝑔) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}} ∈ (𝑆 ↑ko 𝑅)) |
| 52 | | imaeq2 6074 |
. . . . . . . . 9
⊢ (𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → (◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) = (◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})) |
| 53 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) = (𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) |
| 54 | 53 | mptpreima 6258 |
. . . . . . . . 9
⊢ (◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) = {𝑔 ∈ (𝑅 Cn 𝑆) ∣ (𝐹 ∘ 𝑔) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}} |
| 55 | 52, 54 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → (◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) = {𝑔 ∈ (𝑅 Cn 𝑆) ∣ (𝐹 ∘ 𝑔) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}}) |
| 56 | 55 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → ((◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) ∈ (𝑆 ↑ko 𝑅) ↔ {𝑔 ∈ (𝑅 Cn 𝑆) ∣ (𝐹 ∘ 𝑔) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}} ∈ (𝑆 ↑ko 𝑅))) |
| 57 | 51, 56 | syl5ibrcom 247 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 ↾t 𝑘) ∈ Comp) → (𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣} → (◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) ∈ (𝑆 ↑ko 𝑅))) |
| 58 | 57 | expimpd 453 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝒫 ∪ 𝑅
∧ 𝑣 ∈ 𝑇)) → (((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) → (◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) ∈ (𝑆 ↑ko 𝑅))) |
| 59 | 58 | rexlimdvva 3213 |
. . . 4
⊢ (𝜑 → (∃𝑘 ∈ 𝒫 ∪ 𝑅∃𝑣 ∈ 𝑇 ((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑥 = {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) → (◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) ∈ (𝑆 ↑ko 𝑅))) |
| 60 | 11, 59 | biimtrid 242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) → (◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) ∈ (𝑆 ↑ko 𝑅))) |
| 61 | 60 | ralrimiv 3145 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})(◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) ∈ (𝑆 ↑ko 𝑅)) |
| 62 | | eqid 2737 |
. . . . 5
⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅) |
| 63 | 62 | xkotopon 23608 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆))) |
| 64 | 38, 41, 63 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝑆 ↑ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆))) |
| 65 | | ovex 7464 |
. . . . . 6
⊢ (𝑅 Cn 𝑇) ∈ V |
| 66 | 65 | pwex 5380 |
. . . . 5
⊢ 𝒫
(𝑅 Cn 𝑇) ∈ V |
| 67 | 7, 8, 9 | xkotf 23593 |
. . . . . 6
⊢ (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}):({𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp} × 𝑇)⟶𝒫 (𝑅 Cn 𝑇) |
| 68 | | frn 6743 |
. . . . . 6
⊢ ((𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}):({𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp} × 𝑇)⟶𝒫 (𝑅 Cn 𝑇) → ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑇)) |
| 69 | 67, 68 | ax-mp 5 |
. . . . 5
⊢ ran
(𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑇) |
| 70 | 66, 69 | ssexi 5322 |
. . . 4
⊢ ran
(𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ∈ V |
| 71 | 70 | a1i 11 |
. . 3
⊢ (𝜑 → ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣}) ∈ V) |
| 72 | | cntop2 23249 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top) |
| 73 | 2, 72 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ Top) |
| 74 | 7, 8, 9 | xkoval 23595 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑ko 𝑅) = (topGen‘(fi‘ran
(𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})))) |
| 75 | 38, 73, 74 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝑇 ↑ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})))) |
| 76 | | eqid 2737 |
. . . . 5
⊢ (𝑇 ↑ko 𝑅) = (𝑇 ↑ko 𝑅) |
| 77 | 76 | xkotopon 23608 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑇))) |
| 78 | 38, 73, 77 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝑇 ↑ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑇))) |
| 79 | 64, 71, 75, 78 | subbascn 23262 |
. 2
⊢ (𝜑 → ((𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) ∈ ((𝑆 ↑ko 𝑅) Cn (𝑇 ↑ko 𝑅)) ↔ ((𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)):(𝑅 Cn 𝑆)⟶(𝑅 Cn 𝑇) ∧ ∀𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 ∪ 𝑅
∣ (𝑅
↾t 𝑦)
∈ Comp}, 𝑣 ∈
𝑇 ↦ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝑘) ⊆ 𝑣})(◡(𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) “ 𝑥) ∈ (𝑆 ↑ko 𝑅)))) |
| 80 | 6, 61, 79 | mpbir2and 713 |
1
⊢ (𝜑 → (𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) ∈ ((𝑆 ↑ko 𝑅) Cn (𝑇 ↑ko 𝑅))) |