MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkoco1cn Structured version   Visualization version   GIF version

Theorem xkoco1cn 23560
Description: If 𝐹 is a continuous function, then 𝑔 ↦ 𝑔 ∘ 𝐹 is a continuous function on function spaces. (The reason we prove this and xkoco2cn 23561 independently of the more general xkococn 23563 is because that requires some inconvenient extra assumptions on 𝑆.) (Contributed by Mario Carneiro, 20-Mar-2015.)
Hypotheses
Ref Expression
xkoco1cn.t (πœ‘ β†’ 𝑇 ∈ Top)
xkoco1cn.f (πœ‘ β†’ 𝐹 ∈ (𝑅 Cn 𝑆))
Assertion
Ref Expression
xkoco1cn (πœ‘ β†’ (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) ∈ ((𝑇 ↑ko 𝑆) Cn (𝑇 ↑ko 𝑅)))
Distinct variable groups:   πœ‘,𝑔   𝑅,𝑔   𝑆,𝑔   𝑇,𝑔   𝑔,𝐹

Proof of Theorem xkoco1cn
Dummy variables π‘˜ 𝑣 π‘₯ β„Ž 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkoco1cn.f . . . 4 (πœ‘ β†’ 𝐹 ∈ (𝑅 Cn 𝑆))
2 cnco 23169 . . . 4 ((𝐹 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑆 Cn 𝑇)) β†’ (𝑔 ∘ 𝐹) ∈ (𝑅 Cn 𝑇))
31, 2sylan 579 . . 3 ((πœ‘ ∧ 𝑔 ∈ (𝑆 Cn 𝑇)) β†’ (𝑔 ∘ 𝐹) ∈ (𝑅 Cn 𝑇))
43fmpttd 7125 . 2 (πœ‘ β†’ (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)):(𝑆 Cn 𝑇)⟢(𝑅 Cn 𝑇))
5 eqid 2728 . . . . . 6 βˆͺ 𝑅 = βˆͺ 𝑅
6 eqid 2728 . . . . . 6 {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp} = {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}
7 eqid 2728 . . . . . 6 (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) = (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣})
85, 6, 7xkobval 23489 . . . . 5 ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) = {π‘₯ ∣ βˆƒπ‘˜ ∈ 𝒫 βˆͺ π‘…βˆƒπ‘£ ∈ 𝑇 ((𝑅 β†Ύt π‘˜) ∈ Comp ∧ π‘₯ = {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣})}
98eqabri 2873 . . . 4 (π‘₯ ∈ ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) ↔ βˆƒπ‘˜ ∈ 𝒫 βˆͺ π‘…βˆƒπ‘£ ∈ 𝑇 ((𝑅 β†Ύt π‘˜) ∈ Comp ∧ π‘₯ = {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}))
101ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ 𝐹 ∈ (𝑅 Cn 𝑆))
1110, 2sylan 579 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) ∧ 𝑔 ∈ (𝑆 Cn 𝑇)) β†’ (𝑔 ∘ 𝐹) ∈ (𝑅 Cn 𝑇))
12 imaeq1 6058 . . . . . . . . . . . . 13 (β„Ž = (𝑔 ∘ 𝐹) β†’ (β„Ž β€œ π‘˜) = ((𝑔 ∘ 𝐹) β€œ π‘˜))
13 imaco 6255 . . . . . . . . . . . . 13 ((𝑔 ∘ 𝐹) β€œ π‘˜) = (𝑔 β€œ (𝐹 β€œ π‘˜))
1412, 13eqtrdi 2784 . . . . . . . . . . . 12 (β„Ž = (𝑔 ∘ 𝐹) β†’ (β„Ž β€œ π‘˜) = (𝑔 β€œ (𝐹 β€œ π‘˜)))
1514sseq1d 4011 . . . . . . . . . . 11 (β„Ž = (𝑔 ∘ 𝐹) β†’ ((β„Ž β€œ π‘˜) βŠ† 𝑣 ↔ (𝑔 β€œ (𝐹 β€œ π‘˜)) βŠ† 𝑣))
1615elrab3 3683 . . . . . . . . . 10 ((𝑔 ∘ 𝐹) ∈ (𝑅 Cn 𝑇) β†’ ((𝑔 ∘ 𝐹) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣} ↔ (𝑔 β€œ (𝐹 β€œ π‘˜)) βŠ† 𝑣))
1711, 16syl 17 . . . . . . . . 9 ((((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) ∧ 𝑔 ∈ (𝑆 Cn 𝑇)) β†’ ((𝑔 ∘ 𝐹) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣} ↔ (𝑔 β€œ (𝐹 β€œ π‘˜)) βŠ† 𝑣))
1817rabbidva 3436 . . . . . . . 8 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 ∘ 𝐹) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}} = {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 β€œ (𝐹 β€œ π‘˜)) βŠ† 𝑣})
19 eqid 2728 . . . . . . . . 9 βˆͺ 𝑆 = βˆͺ 𝑆
20 cntop2 23144 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 Cn 𝑆) β†’ 𝑆 ∈ Top)
211, 20syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 ∈ Top)
2221ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ 𝑆 ∈ Top)
23 xkoco1cn.t . . . . . . . . . 10 (πœ‘ β†’ 𝑇 ∈ Top)
2423ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ 𝑇 ∈ Top)
25 imassrn 6074 . . . . . . . . . 10 (𝐹 β€œ π‘˜) βŠ† ran 𝐹
265, 19cnf 23149 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 Cn 𝑆) β†’ 𝐹:βˆͺ π‘…βŸΆβˆͺ 𝑆)
27 frn 6729 . . . . . . . . . . 11 (𝐹:βˆͺ π‘…βŸΆβˆͺ 𝑆 β†’ ran 𝐹 βŠ† βˆͺ 𝑆)
2810, 26, 273syl 18 . . . . . . . . . 10 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ ran 𝐹 βŠ† βˆͺ 𝑆)
2925, 28sstrid 3991 . . . . . . . . 9 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ (𝐹 β€œ π‘˜) βŠ† βˆͺ 𝑆)
30 imacmp 23300 . . . . . . . . . 10 ((𝐹 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ (𝑆 β†Ύt (𝐹 β€œ π‘˜)) ∈ Comp)
3110, 30sylancom 587 . . . . . . . . 9 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ (𝑆 β†Ύt (𝐹 β€œ π‘˜)) ∈ Comp)
32 simplrr 777 . . . . . . . . 9 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ 𝑣 ∈ 𝑇)
3319, 22, 24, 29, 31, 32xkoopn 23492 . . . . . . . 8 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 β€œ (𝐹 β€œ π‘˜)) βŠ† 𝑣} ∈ (𝑇 ↑ko 𝑆))
3418, 33eqeltrd 2829 . . . . . . 7 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 ∘ 𝐹) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}} ∈ (𝑇 ↑ko 𝑆))
35 imaeq2 6059 . . . . . . . . 9 (π‘₯ = {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣} β†’ (β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) = (β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}))
36 eqid 2728 . . . . . . . . . 10 (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) = (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹))
3736mptpreima 6242 . . . . . . . . 9 (β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) = {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 ∘ 𝐹) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}}
3835, 37eqtrdi 2784 . . . . . . . 8 (π‘₯ = {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣} β†’ (β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) = {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 ∘ 𝐹) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}})
3938eleq1d 2814 . . . . . . 7 (π‘₯ = {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣} β†’ ((β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) ∈ (𝑇 ↑ko 𝑆) ↔ {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 ∘ 𝐹) ∈ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}} ∈ (𝑇 ↑ko 𝑆)))
4034, 39syl5ibrcom 246 . . . . . 6 (((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) ∧ (𝑅 β†Ύt π‘˜) ∈ Comp) β†’ (π‘₯ = {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣} β†’ (β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) ∈ (𝑇 ↑ko 𝑆)))
4140expimpd 453 . . . . 5 ((πœ‘ ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑅 ∧ 𝑣 ∈ 𝑇)) β†’ (((𝑅 β†Ύt π‘˜) ∈ Comp ∧ π‘₯ = {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) β†’ (β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) ∈ (𝑇 ↑ko 𝑆)))
4241rexlimdvva 3208 . . . 4 (πœ‘ β†’ (βˆƒπ‘˜ ∈ 𝒫 βˆͺ π‘…βˆƒπ‘£ ∈ 𝑇 ((𝑅 β†Ύt π‘˜) ∈ Comp ∧ π‘₯ = {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) β†’ (β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) ∈ (𝑇 ↑ko 𝑆)))
439, 42biimtrid 241 . . 3 (πœ‘ β†’ (π‘₯ ∈ ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) β†’ (β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) ∈ (𝑇 ↑ko 𝑆)))
4443ralrimiv 3142 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣})(β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) ∈ (𝑇 ↑ko 𝑆))
45 eqid 2728 . . . . 5 (𝑇 ↑ko 𝑆) = (𝑇 ↑ko 𝑆)
4645xkotopon 23503 . . . 4 ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) β†’ (𝑇 ↑ko 𝑆) ∈ (TopOnβ€˜(𝑆 Cn 𝑇)))
4721, 23, 46syl2anc 583 . . 3 (πœ‘ β†’ (𝑇 ↑ko 𝑆) ∈ (TopOnβ€˜(𝑆 Cn 𝑇)))
48 ovex 7453 . . . . . 6 (𝑅 Cn 𝑇) ∈ V
4948pwex 5380 . . . . 5 𝒫 (𝑅 Cn 𝑇) ∈ V
505, 6, 7xkotf 23488 . . . . . 6 (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}):({𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp} Γ— 𝑇)βŸΆπ’« (𝑅 Cn 𝑇)
51 frn 6729 . . . . . 6 ((π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}):({𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp} Γ— 𝑇)βŸΆπ’« (𝑅 Cn 𝑇) β†’ ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) βŠ† 𝒫 (𝑅 Cn 𝑇))
5250, 51ax-mp 5 . . . . 5 ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) βŠ† 𝒫 (𝑅 Cn 𝑇)
5349, 52ssexi 5322 . . . 4 ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) ∈ V
5453a1i 11 . . 3 (πœ‘ β†’ ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}) ∈ V)
55 cntop1 23143 . . . . 5 (𝐹 ∈ (𝑅 Cn 𝑆) β†’ 𝑅 ∈ Top)
561, 55syl 17 . . . 4 (πœ‘ β†’ 𝑅 ∈ Top)
575, 6, 7xkoval 23490 . . . 4 ((𝑅 ∈ Top ∧ 𝑇 ∈ Top) β†’ (𝑇 ↑ko 𝑅) = (topGenβ€˜(fiβ€˜ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}))))
5856, 23, 57syl2anc 583 . . 3 (πœ‘ β†’ (𝑇 ↑ko 𝑅) = (topGenβ€˜(fiβ€˜ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣}))))
59 eqid 2728 . . . . 5 (𝑇 ↑ko 𝑅) = (𝑇 ↑ko 𝑅)
6059xkotopon 23503 . . . 4 ((𝑅 ∈ Top ∧ 𝑇 ∈ Top) β†’ (𝑇 ↑ko 𝑅) ∈ (TopOnβ€˜(𝑅 Cn 𝑇)))
6156, 23, 60syl2anc 583 . . 3 (πœ‘ β†’ (𝑇 ↑ko 𝑅) ∈ (TopOnβ€˜(𝑅 Cn 𝑇)))
6247, 54, 58, 61subbascn 23157 . 2 (πœ‘ β†’ ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) ∈ ((𝑇 ↑ko 𝑆) Cn (𝑇 ↑ko 𝑅)) ↔ ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)):(𝑆 Cn 𝑇)⟢(𝑅 Cn 𝑇) ∧ βˆ€π‘₯ ∈ ran (π‘˜ ∈ {𝑦 ∈ 𝒫 βˆͺ 𝑅 ∣ (𝑅 β†Ύt 𝑦) ∈ Comp}, 𝑣 ∈ 𝑇 ↦ {β„Ž ∈ (𝑅 Cn 𝑇) ∣ (β„Ž β€œ π‘˜) βŠ† 𝑣})(β—‘(𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) β€œ π‘₯) ∈ (𝑇 ↑ko 𝑆))))
634, 44, 62mpbir2and 712 1 (πœ‘ β†’ (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) ∈ ((𝑇 ↑ko 𝑆) Cn (𝑇 ↑ko 𝑅)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  βˆ€wral 3058  βˆƒwrex 3067  {crab 3429  Vcvv 3471   βŠ† wss 3947  π’« cpw 4603  βˆͺ cuni 4908   ↦ cmpt 5231   Γ— cxp 5676  β—‘ccnv 5677  ran crn 5679   β€œ cima 5681   ∘ ccom 5682  βŸΆwf 6544  β€˜cfv 6548  (class class class)co 7420   ∈ cmpo 7422  ficfi 9433   β†Ύt crest 17401  topGenctg 17418  Topctop 22794  TopOnctopon 22811   Cn ccn 23127  Compccmp 23289   ↑ko cxko 23464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-1o 8486  df-er 8724  df-map 8846  df-en 8964  df-dom 8965  df-fin 8967  df-fi 9434  df-rest 17403  df-topgen 17424  df-top 22795  df-topon 22812  df-bases 22848  df-cn 23130  df-cmp 23290  df-xko 23466
This theorem is referenced by:  cnmpt1k  23585
  Copyright terms: Public domain W3C validator