Metamath Proof Explorer

Theorem xkoco1cn

Description: If F is a continuous function, then g |-> g o. F is a continuous function on function spaces. (The reason we prove this and xkoco2cn independently of the more general xkococn is because that requires some inconvenient extra assumptions on S .) (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Hypotheses xkoco1cn.t ⊢ ( 𝜑 → 𝑇 ∈ Top )
xkoco1cn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 Cn 𝑆 ) )
Assertion xkoco1cn ( 𝜑 → ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( ( 𝑇 ↑ko 𝑆 ) Cn ( 𝑇 ↑ko 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 xkoco1cn.t ⊢ ( 𝜑 → 𝑇 ∈ Top )
2 xkoco1cn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 Cn 𝑆 ) )
3 cnco ⊢ ( ( 𝐹 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ) → ( 𝑔 ∘ 𝐹 ) ∈ ( 𝑅 Cn 𝑇 ) )
4 2 3 sylan ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ) → ( 𝑔 ∘ 𝐹 ) ∈ ( 𝑅 Cn 𝑇 ) )
5 4 fmpttd ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) : ( 𝑆 Cn 𝑇 ) ⟶ ( 𝑅 Cn 𝑇 ) )
6 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
7 eqid ⊢ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } = { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp }
8 eqid ⊢ ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } )
9 6 7 8 xkobval ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑥 ∣ ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑇 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) }
10 9 eqabri ⊢ ( 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ↔ ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑇 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
11 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝐹 ∈ ( 𝑅 Cn 𝑆 ) )
12 11 3 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ) → ( 𝑔 ∘ 𝐹 ) ∈ ( 𝑅 Cn 𝑇 ) )
13 imaeq1 ⊢ ( ℎ = ( 𝑔 ∘ 𝐹 ) → ( ℎ “ 𝑘 ) = ( ( 𝑔 ∘ 𝐹 ) “ 𝑘 ) )
14 imaco ⊢ ( ( 𝑔 ∘ 𝐹 ) “ 𝑘 ) = ( 𝑔 “ ( 𝐹 “ 𝑘 ) )
15 13 14 eqtrdi ⊢ ( ℎ = ( 𝑔 ∘ 𝐹 ) → ( ℎ “ 𝑘 ) = ( 𝑔 “ ( 𝐹 “ 𝑘 ) ) )
16 15 sseq1d ⊢ ( ℎ = ( 𝑔 ∘ 𝐹 ) → ( ( ℎ “ 𝑘 ) ⊆ 𝑣 ↔ ( 𝑔 “ ( 𝐹 “ 𝑘 ) ) ⊆ 𝑣 ) )
17 16 elrab3 ⊢ ( ( 𝑔 ∘ 𝐹 ) ∈ ( 𝑅 Cn 𝑇 ) → ( ( 𝑔 ∘ 𝐹 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ( 𝑔 “ ( 𝐹 “ 𝑘 ) ) ⊆ 𝑣 ) )
18 12 17 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ) → ( ( 𝑔 ∘ 𝐹 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ( 𝑔 “ ( 𝐹 “ 𝑘 ) ) ⊆ 𝑣 ) )
19 18 rabbidva ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → { 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑔 ∘ 𝐹 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } = { 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑔 “ ( 𝐹 “ 𝑘 ) ) ⊆ 𝑣 } )
20 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
21 cntop2 ⊢ ( 𝐹 ∈ ( 𝑅 Cn 𝑆 ) → 𝑆 ∈ Top )
22 2 21 syl ⊢ ( 𝜑 → 𝑆 ∈ Top )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑆 ∈ Top )
24 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑇 ∈ Top )
25 imassrn ⊢ ( 𝐹 “ 𝑘 ) ⊆ ran 𝐹
26 6 20 cnf ⊢ ( 𝐹 ∈ ( 𝑅 Cn 𝑆 ) → 𝐹 : ∪ 𝑅 ⟶ ∪ 𝑆 )
27 frn ⊢ ( 𝐹 : ∪ 𝑅 ⟶ ∪ 𝑆 → ran 𝐹 ⊆ ∪ 𝑆 )
28 11 26 27 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ran 𝐹 ⊆ ∪ 𝑆 )
29 25 28 sstrid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( 𝐹 “ 𝑘 ) ⊆ ∪ 𝑆 )
30 imacmp ⊢ ( ( 𝐹 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( 𝑆 ↾t ( 𝐹 “ 𝑘 ) ) ∈ Comp )
31 11 30 sylancom ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( 𝑆 ↾t ( 𝐹 “ 𝑘 ) ) ∈ Comp )
32 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑣 ∈ 𝑇 )
33 20 23 24 29 31 32 xkoopn ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → { 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑔 “ ( 𝐹 “ 𝑘 ) ) ⊆ 𝑣 } ∈ ( 𝑇 ↑ko 𝑆 ) )
34 19 33 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → { 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑔 ∘ 𝐹 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } ∈ ( 𝑇 ↑ko 𝑆 ) )
35 imaeq2 ⊢ ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) = ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
36 eqid ⊢ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) = ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) )
37 36 mptpreima ⊢ ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑔 ∘ 𝐹 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } }
38 35 37 eqtrdi ⊢ ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) = { 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑔 ∘ 𝐹 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } )
39 38 eleq1d ⊢ ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) ∈ ( 𝑇 ↑ko 𝑆 ) ↔ { 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑔 ∘ 𝐹 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } ∈ ( 𝑇 ↑ko 𝑆 ) ) )
40 34 39 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) ∈ ( 𝑇 ↑ko 𝑆 ) ) )
41 40 expimpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) → ( ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) ∈ ( 𝑇 ↑ko 𝑆 ) ) )
42 41 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑇 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) ∈ ( 𝑇 ↑ko 𝑆 ) ) )
43 10 42 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) ∈ ( 𝑇 ↑ko 𝑆 ) ) )
44 43 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) ∈ ( 𝑇 ↑ko 𝑆 ) )
45 eqid ⊢ ( 𝑇 ↑ko 𝑆 ) = ( 𝑇 ↑ko 𝑆 )
46 45 xkotopon ⊢ ( ( 𝑆 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑆 ) ∈ ( TopOn ‘ ( 𝑆 Cn 𝑇 ) ) )
47 22 1 46 syl2anc ⊢ ( 𝜑 → ( 𝑇 ↑ko 𝑆 ) ∈ ( TopOn ‘ ( 𝑆 Cn 𝑇 ) ) )
48 ovex ⊢ ( 𝑅 Cn 𝑇 ) ∈ V
49 48 pwex ⊢ 𝒫 ( 𝑅 Cn 𝑇 ) ∈ V
50 6 7 8 xkotf ⊢ ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } × 𝑇 ) ⟶ 𝒫 ( 𝑅 Cn 𝑇 )
51 frn ⊢ ( ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } × 𝑇 ) ⟶ 𝒫 ( 𝑅 Cn 𝑇 ) → ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑇 ) )
52 50 51 ax-mp ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑇 )
53 49 52 ssexi ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ V
54 53 a1i ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ V )
55 cntop1 ⊢ ( 𝐹 ∈ ( 𝑅 Cn 𝑆 ) → 𝑅 ∈ Top )
56 2 55 syl ⊢ ( 𝜑 → 𝑅 ∈ Top )
57 6 7 8 xkoval ⊢ ( ( 𝑅 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
58 56 1 57 syl2anc ⊢ ( 𝜑 → ( 𝑇 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
59 eqid ⊢ ( 𝑇 ↑ko 𝑅 ) = ( 𝑇 ↑ko 𝑅 )
60 59 xkotopon ⊢ ( ( 𝑅 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑇 ) ) )
61 56 1 60 syl2anc ⊢ ( 𝜑 → ( 𝑇 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑇 ) ) )
62 47 54 58 61 subbascn ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( ( 𝑇 ↑ko 𝑆 ) Cn ( 𝑇 ↑ko 𝑅 ) ) ↔ ( ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) : ( 𝑆 Cn 𝑇 ) ⟶ ( 𝑅 Cn 𝑇 ) ∧ ∀ 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) “ 𝑥 ) ∈ ( 𝑇 ↑ko 𝑆 ) ) ) )
63 5 44 62 mpbir2and ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑆 Cn 𝑇 ) ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( ( 𝑇 ↑ko 𝑆 ) Cn ( 𝑇 ↑ko 𝑅 ) ) )