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 𝑅 ) ) )