Metamath Proof Explorer

Theorem xkoco2cn

Description: If F is a continuous function, then g |-> F o. g is a continuous function on function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 xkoco2cn.r ⊢ ( 𝜑 → 𝑅 ∈ Top )
2 xkoco2cn.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 Cn 𝑇 ) )
3 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝑔 ∈ ( 𝑅 Cn 𝑆 ) )
4 2 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝐹 ∈ ( 𝑆 Cn 𝑇 ) )
5 cnco ⊢ ( ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝐹 ∈ ( 𝑆 Cn 𝑇 ) ) → ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑅 Cn 𝑇 ) )
6 3 4 5 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑅 Cn 𝑇 ) )
7 6 fmpttd ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) : ( 𝑅 Cn 𝑆 ) ⟶ ( 𝑅 Cn 𝑇 ) )
8 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
9 eqid ⊢ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } = { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp }
10 eqid ⊢ ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } )
11 8 9 10 xkobval ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑥 ∣ ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑇 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) }
12 11 abeq2i ⊢ ( 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ↔ ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑇 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
13 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝑔 ∈ ( 𝑅 Cn 𝑆 ) )
14 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝐹 ∈ ( 𝑆 Cn 𝑇 ) )
15 13 14 5 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑅 Cn 𝑇 ) )
16 imaeq1 ⊢ ( ℎ = ( 𝐹 ∘ 𝑔 ) → ( ℎ “ 𝑘 ) = ( ( 𝐹 ∘ 𝑔 ) “ 𝑘 ) )
17 imaco ⊢ ( ( 𝐹 ∘ 𝑔 ) “ 𝑘 ) = ( 𝐹 “ ( 𝑔 “ 𝑘 ) )
18 16 17 eqtrdi ⊢ ( ℎ = ( 𝐹 ∘ 𝑔 ) → ( ℎ “ 𝑘 ) = ( 𝐹 “ ( 𝑔 “ 𝑘 ) ) )
19 18 sseq1d ⊢ ( ℎ = ( 𝐹 ∘ 𝑔 ) → ( ( ℎ “ 𝑘 ) ⊆ 𝑣 ↔ ( 𝐹 “ ( 𝑔 “ 𝑘 ) ) ⊆ 𝑣 ) )
20 19 elrab3 ⊢ ( ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑅 Cn 𝑇 ) → ( ( 𝐹 ∘ 𝑔 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ( 𝐹 “ ( 𝑔 “ 𝑘 ) ) ⊆ 𝑣 ) )
21 15 20 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( 𝐹 ∘ 𝑔 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ( 𝐹 “ ( 𝑔 “ 𝑘 ) ) ⊆ 𝑣 ) )
22 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
23 eqid ⊢ ∪ 𝑇 = ∪ 𝑇
24 22 23 cnf ⊢ ( 𝐹 ∈ ( 𝑆 Cn 𝑇 ) → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
25 2 24 syl ⊢ ( 𝜑 → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
26 25 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝐹 : ∪ 𝑆 ⟶ ∪ 𝑇 )
27 26 ffund ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → Fun 𝐹 )
28 imassrn ⊢ ( 𝑔 “ 𝑘 ) ⊆ ran 𝑔
29 8 22 cnf ⊢ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) → 𝑔 : ∪ 𝑅 ⟶ ∪ 𝑆 )
30 13 29 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝑔 : ∪ 𝑅 ⟶ ∪ 𝑆 )
31 30 frnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ran 𝑔 ⊆ ∪ 𝑆 )
32 28 31 sstrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑔 “ 𝑘 ) ⊆ ∪ 𝑆 )
33 26 fdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → dom 𝐹 = ∪ 𝑆 )
34 32 33 sseqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑔 “ 𝑘 ) ⊆ dom 𝐹 )
35 funimass3 ⊢ ( ( Fun 𝐹 ∧ ( 𝑔 “ 𝑘 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝑔 “ 𝑘 ) ) ⊆ 𝑣 ↔ ( 𝑔 “ 𝑘 ) ⊆ ( ◡ 𝐹 “ 𝑣 ) ) )
36 27 34 35 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( 𝐹 “ ( 𝑔 “ 𝑘 ) ) ⊆ 𝑣 ↔ ( 𝑔 “ 𝑘 ) ⊆ ( ◡ 𝐹 “ 𝑣 ) ) )
37 21 36 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( 𝐹 ∘ 𝑔 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ( 𝑔 “ 𝑘 ) ⊆ ( ◡ 𝐹 “ 𝑣 ) ) )
38 37 rabbidva ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → { 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝐹 ∘ 𝑔 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } = { 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑔 “ 𝑘 ) ⊆ ( ◡ 𝐹 “ 𝑣 ) } )
39 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑅 ∈ Top )
40 cntop1 ⊢ ( 𝐹 ∈ ( 𝑆 Cn 𝑇 ) → 𝑆 ∈ Top )
41 2 40 syl ⊢ ( 𝜑 → 𝑆 ∈ Top )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑆 ∈ Top )
43 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑘 ∈ 𝒫 ∪ 𝑅 )
44 43 elpwid ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑘 ⊆ ∪ 𝑅 )
45 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( 𝑅 ↾t 𝑘 ) ∈ Comp )
46 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝐹 ∈ ( 𝑆 Cn 𝑇 ) )
47 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑣 ∈ 𝑇 )
48 cnima ⊢ ( ( 𝐹 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑣 ∈ 𝑇 ) → ( ◡ 𝐹 “ 𝑣 ) ∈ 𝑆 )
49 46 47 48 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( ◡ 𝐹 “ 𝑣 ) ∈ 𝑆 )
50 8 39 42 44 45 49 xkoopn ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → { 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑔 “ 𝑘 ) ⊆ ( ◡ 𝐹 “ 𝑣 ) } ∈ ( 𝑆 ↑ko 𝑅 ) )
51 38 50 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → { 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝐹 ∘ 𝑔 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } ∈ ( 𝑆 ↑ko 𝑅 ) )
52 imaeq2 ⊢ ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) = ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
53 eqid ⊢ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) = ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) )
54 53 mptpreima ⊢ ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝐹 ∘ 𝑔 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } }
55 52 54 eqtrdi ⊢ ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) = { 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝐹 ∘ 𝑔 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } )
56 55 eleq1d ⊢ ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) ∈ ( 𝑆 ↑ko 𝑅 ) ↔ { 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝐹 ∘ 𝑔 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } ∈ ( 𝑆 ↑ko 𝑅 ) ) )
57 51 56 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) ∈ ( 𝑆 ↑ko 𝑅 ) ) )
58 57 expimpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑇 ) ) → ( ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) ∈ ( 𝑆 ↑ko 𝑅 ) ) )
59 58 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑇 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) ∈ ( 𝑆 ↑ko 𝑅 ) ) )
60 12 59 syl5bi ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) ∈ ( 𝑆 ↑ko 𝑅 ) ) )
61 60 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) ∈ ( 𝑆 ↑ko 𝑅 ) )
62 eqid ⊢ ( 𝑆 ↑ko 𝑅 ) = ( 𝑆 ↑ko 𝑅 )
63 62 xkotopon ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
64 1 41 63 syl2anc ⊢ ( 𝜑 → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
65 ovex ⊢ ( 𝑅 Cn 𝑇 ) ∈ V
66 65 pwex ⊢ 𝒫 ( 𝑅 Cn 𝑇 ) ∈ V
67 8 9 10 xkotf ⊢ ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } × 𝑇 ) ⟶ 𝒫 ( 𝑅 Cn 𝑇 )
68 frn ⊢ ( ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } × 𝑇 ) ⟶ 𝒫 ( 𝑅 Cn 𝑇 ) → ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑇 ) )
69 67 68 ax-mp ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑇 )
70 66 69 ssexi ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ V
71 70 a1i ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ V )
72 cntop2 ⊢ ( 𝐹 ∈ ( 𝑆 Cn 𝑇 ) → 𝑇 ∈ Top )
73 2 72 syl ⊢ ( 𝜑 → 𝑇 ∈ Top )
74 8 9 10 xkoval ⊢ ( ( 𝑅 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
75 1 73 74 syl2anc ⊢ ( 𝜑 → ( 𝑇 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
76 eqid ⊢ ( 𝑇 ↑ko 𝑅 ) = ( 𝑇 ↑ko 𝑅 )
77 76 xkotopon ⊢ ( ( 𝑅 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑇 ) ) )
78 1 73 77 syl2anc ⊢ ( 𝜑 → ( 𝑇 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑇 ) ) )
79 64 71 75 78 subbascn ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) ∈ ( ( 𝑆 ↑ko 𝑅 ) Cn ( 𝑇 ↑ko 𝑅 ) ) ↔ ( ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) : ( 𝑅 Cn 𝑆 ) ⟶ ( 𝑅 Cn 𝑇 ) ∧ ∀ 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) “ 𝑥 ) ∈ ( 𝑆 ↑ko 𝑅 ) ) ) )
80 7 61 79 mpbir2and ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝐹 ∘ 𝑔 ) ) ∈ ( ( 𝑆 ↑ko 𝑅 ) Cn ( 𝑇 ↑ko 𝑅 ) ) )