Metamath Proof Explorer

Theorem xkococn

Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis xkococn.1 ⊢ 𝐹 = ( 𝑓 ∈ ( 𝑆 Cn 𝑇 ) , 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑓 ∘ 𝑔 ) )
Assertion xkococn ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → 𝐹 ∈ ( ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) Cn ( 𝑇 ↑ko 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 xkococn.1 ⊢ 𝐹 = ( 𝑓 ∈ ( 𝑆 Cn 𝑇 ) , 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑓 ∘ 𝑔 ) )
2 simprr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑓 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → 𝑔 ∈ ( 𝑅 Cn 𝑆 ) )
3 simprl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑓 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → 𝑓 ∈ ( 𝑆 Cn 𝑇 ) )
4 cnco ⊢ ( ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑓 ∈ ( 𝑆 Cn 𝑇 ) ) → ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 Cn 𝑇 ) )
5 2 3 4 syl2anc ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑓 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 Cn 𝑇 ) )
6 5 ralrimivva ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ∀ 𝑓 ∈ ( 𝑆 Cn 𝑇 ) ∀ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 Cn 𝑇 ) )
7 1 fmpo ⊢ ( ∀ 𝑓 ∈ ( 𝑆 Cn 𝑇 ) ∀ 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 Cn 𝑇 ) ↔ 𝐹 : ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ⟶ ( 𝑅 Cn 𝑇 ) )
8 6 7 sylib ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → 𝐹 : ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ⟶ ( 𝑅 Cn 𝑇 ) )
9 eqid ⊢ ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } )
10 9 rnmpo ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑥 ∣ ∃ 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } }
11 10 eleq2i ⊢ ( 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ↔ 𝑥 ∈ { 𝑥 ∣ ∃ 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } )
12 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } } ↔ ∃ 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } )
13 oveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝑅 ↾t 𝑦 ) = ( 𝑅 ↾t 𝑘 ) )
14 13 eleq1d ⊢ ( 𝑦 = 𝑘 → ( ( 𝑅 ↾t 𝑦 ) ∈ Comp ↔ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) )
15 14 rexrab ⊢ ( ∃ 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
16 11 12 15 3bitri ⊢ ( 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ↔ ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
17 8 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → 𝐹 : ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ⟶ ( 𝑅 Cn 𝑇 ) )
18 ffn ⊢ ( 𝐹 : ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ⟶ ( 𝑅 Cn 𝑇 ) → 𝐹 Fn ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) )
19 elpreima ⊢ ( 𝐹 Fn ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) → ( 𝑦 ∈ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ↔ ( 𝑦 ∈ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) )
20 17 18 19 3syl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ( 𝑦 ∈ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ↔ ( 𝑦 ∈ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) )
21 coeq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 ∘ 𝑔 ) = ( 𝑎 ∘ 𝑔 ) )
22 coeq2 ⊢ ( 𝑔 = 𝑏 → ( 𝑎 ∘ 𝑔 ) = ( 𝑎 ∘ 𝑏 ) )
23 vex ⊢ 𝑎 ∈ V
24 vex ⊢ 𝑏 ∈ V
25 23 24 coex ⊢ ( 𝑎 ∘ 𝑏 ) ∈ V
26 21 22 1 25 ovmpo ⊢ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑎 𝐹 𝑏 ) = ( 𝑎 ∘ 𝑏 ) )
27 26 adantl ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( 𝑎 𝐹 𝑏 ) = ( 𝑎 ∘ 𝑏 ) )
28 27 eleq1d ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( ( 𝑎 𝐹 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ( 𝑎 ∘ 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
29 imaeq1 ⊢ ( ℎ = ( 𝑎 ∘ 𝑏 ) → ( ℎ “ 𝑘 ) = ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) )
30 29 sseq1d ⊢ ( ℎ = ( 𝑎 ∘ 𝑏 ) → ( ( ℎ “ 𝑘 ) ⊆ 𝑣 ↔ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) )
31 30 elrab ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ( ( 𝑎 ∘ 𝑏 ) ∈ ( 𝑅 Cn 𝑇 ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) )
32 31 simprbi ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 )
33 simp2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → 𝑆 ∈ 𝑛-Locally Comp )
34 33 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) ) → 𝑆 ∈ 𝑛-Locally Comp )
35 elpwi ⊢ ( 𝑘 ∈ 𝒫 ∪ 𝑅 → 𝑘 ⊆ ∪ 𝑅 )
36 35 ad2antrl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) → 𝑘 ⊆ ∪ 𝑅 )
37 36 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) ) → 𝑘 ⊆ ∪ 𝑅 )
38 simprr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑅 ↾t 𝑘 ) ∈ Comp )
39 38 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) ) → ( 𝑅 ↾t 𝑘 ) ∈ Comp )
40 simplr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) ) → 𝑣 ∈ 𝑇 )
41 simprll ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) ) → 𝑎 ∈ ( 𝑆 Cn 𝑇 ) )
42 simprlr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) ) → 𝑏 ∈ ( 𝑅 Cn 𝑆 ) )
43 simprr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) ) → ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 )
44 1 34 37 39 40 41 42 43 xkococnlem ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ∧ ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) )
45 44 expr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( ( ( 𝑎 ∘ 𝑏 ) “ 𝑘 ) ⊆ 𝑣 → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
46 32 45 syl5 ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( ( 𝑎 ∘ 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
47 28 46 sylbid ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ) ) → ( ( 𝑎 𝐹 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
48 47 ralrimivva ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ∀ 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∀ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ( ( 𝑎 𝐹 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
49 fveq2 ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
50 df-ov ⊢ ( 𝑎 𝐹 𝑏 ) = ( 𝐹 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
51 49 50 eqtr4di ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝐹 ‘ 𝑦 ) = ( 𝑎 𝐹 𝑏 ) )
52 51 eleq1d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝐹 ‘ 𝑦 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ↔ ( 𝑎 𝐹 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
53 eleq1 ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑦 ∈ 𝑧 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ) )
54 53 anbi1d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
55 54 rexbidv ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ↔ ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
56 52 55 imbi12d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 𝐹 ‘ 𝑦 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) ↔ ( ( 𝑎 𝐹 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) ) )
57 56 ralxp ⊢ ( ∀ 𝑦 ∈ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ( ( 𝐹 ‘ 𝑦 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) ↔ ∀ 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∀ 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ( ( 𝑎 𝐹 𝑏 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
58 48 57 sylibr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ∀ 𝑦 ∈ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ( ( 𝐹 ‘ 𝑦 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
59 58 r19.21bi ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) ∧ 𝑦 ∈ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ) → ( ( 𝐹 ‘ 𝑦 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
60 59 expimpd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ( ( 𝑦 ∈ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
61 20 60 sylbid ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ( 𝑦 ∈ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
62 61 ralrimiv ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ∀ 𝑦 ∈ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) )
63 nllytop ⊢ ( 𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top )
64 63 3ad2ant2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → 𝑆 ∈ Top )
65 simp3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → 𝑇 ∈ Top )
66 xkotop ⊢ ( ( 𝑆 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑆 ) ∈ Top )
67 64 65 66 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑆 ) ∈ Top )
68 simp1 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → 𝑅 ∈ Top )
69 xkotop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ Top )
70 68 64 69 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ Top )
71 txtop ⊢ ( ( ( 𝑇 ↑ko 𝑆 ) ∈ Top ∧ ( 𝑆 ↑ko 𝑅 ) ∈ Top ) → ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ∈ Top )
72 67 70 71 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ∈ Top )
73 72 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ∈ Top )
74 eltop2 ⊢ ( ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ∈ Top → ( ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ↔ ∀ 𝑦 ∈ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
75 73 74 syl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ( ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ↔ ∀ 𝑦 ∈ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
76 62 75 mpbird ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) )
77 imaeq2 ⊢ ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) )
78 77 eleq1d ⊢ ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ↔ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ) )
79 76 78 syl5ibrcom ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑣 ∈ 𝑇 ) → ( 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ) )
80 79 rexlimdva ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ) → ( ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ) )
81 80 anassrs ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ 𝑘 ∈ 𝒫 ∪ 𝑅 ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } → ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ) )
82 81 expimpd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) ∧ 𝑘 ∈ 𝒫 ∪ 𝑅 ) → ( ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ) )
83 82 rexlimdva ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ ∃ 𝑣 ∈ 𝑇 𝑥 = { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ) )
84 16 83 syl5bi ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ) )
85 84 ralrimiv ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ∀ 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) )
86 eqid ⊢ ( 𝑇 ↑ko 𝑆 ) = ( 𝑇 ↑ko 𝑆 )
87 86 xkotopon ⊢ ( ( 𝑆 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑆 ) ∈ ( TopOn ‘ ( 𝑆 Cn 𝑇 ) ) )
88 64 65 87 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑆 ) ∈ ( TopOn ‘ ( 𝑆 Cn 𝑇 ) ) )
89 eqid ⊢ ( 𝑆 ↑ko 𝑅 ) = ( 𝑆 ↑ko 𝑅 )
90 89 xkotopon ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
91 68 64 90 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
92 txtopon ⊢ ( ( ( 𝑇 ↑ko 𝑆 ) ∈ ( TopOn ‘ ( 𝑆 Cn 𝑇 ) ) ∧ ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) ) → ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ∈ ( TopOn ‘ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ) )
93 88 91 92 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ∈ ( TopOn ‘ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ) )
94 ovex ⊢ ( 𝑅 Cn 𝑇 ) ∈ V
95 94 pwex ⊢ 𝒫 ( 𝑅 Cn 𝑇 ) ∈ V
96 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
97 eqid ⊢ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } = { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp }
98 96 97 9 xkotf ⊢ ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } × 𝑇 ) ⟶ 𝒫 ( 𝑅 Cn 𝑇 )
99 frn ⊢ ( ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } × 𝑇 ) ⟶ 𝒫 ( 𝑅 Cn 𝑇 ) → ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑇 ) )
100 98 99 ax-mp ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑇 )
101 95 100 ssexi ⊢ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ V
102 101 a1i ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ∈ V )
103 96 97 9 xkoval ⊢ ( ( 𝑅 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
104 103 3adant2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
105 eqid ⊢ ( 𝑇 ↑ko 𝑅 ) = ( 𝑇 ↑ko 𝑅 )
106 105 xkotopon ⊢ ( ( 𝑅 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑇 ) ) )
107 106 3adant2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑇 ) ) )
108 93 102 104 107 subbascn ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → ( 𝐹 ∈ ( ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) Cn ( 𝑇 ↑ko 𝑅 ) ) ↔ ( 𝐹 : ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) ⟶ ( 𝑅 Cn 𝑇 ) ∧ ∀ 𝑥 ∈ ran ( 𝑘 ∈ { 𝑦 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑦 ) ∈ Comp } , 𝑣 ∈ 𝑇 ↦ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ 𝐹 “ 𝑥 ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ) ) )
109 8 85 108 mpbir2and ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top ) → 𝐹 ∈ ( ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) Cn ( 𝑇 ↑ko 𝑅 ) ) )