Metamath Proof Explorer

Theorem xkoinjcn

Description: Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis xkoinjcn.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) )
Assertion xkoinjcn ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐹 ∈ ( 𝑅 Cn ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 xkoinjcn.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) )
2 simplr ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ ( TopOn ‘ 𝑌 ) )
3 2 cnmptid ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝑦 ) ∈ ( 𝑆 Cn 𝑆 ) )
4 simpll ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
5 simpr ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
6 2 4 5 cnmptc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝑥 ) ∈ ( 𝑆 Cn 𝑅 ) )
7 2 3 6 cnmpt1t ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) )
8 7 1 fmptd ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐹 : 𝑋 ⟶ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) )
9 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
10 eqid ⊢ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } = { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp }
11 eqid ⊢ ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
12 9 10 11 xkobval ⊢ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑧 ∣ ∃ 𝑘 ∈ 𝒫 ∪ 𝑆 ∃ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ( ( 𝑆 ↾t 𝑘 ) ∈ Comp ∧ 𝑧 = { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) }
13 12 eqabri ⊢ ( 𝑧 ∈ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ↔ ∃ 𝑘 ∈ 𝒫 ∪ 𝑆 ∃ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ( ( 𝑆 ↾t 𝑘 ) ∈ Comp ∧ 𝑧 = { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
14 simpll ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) )
15 14 7 sylan ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) )
16 imaeq1 ⊢ ( 𝑓 = ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) → ( 𝑓 “ 𝑘 ) = ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) “ 𝑘 ) )
17 16 sseq1d ⊢ ( 𝑓 = ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) → ( ( 𝑓 “ 𝑘 ) ⊆ 𝑣 ↔ ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) “ 𝑘 ) ⊆ 𝑣 ) )
18 17 elrab3 ⊢ ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) → ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) “ 𝑘 ) ⊆ 𝑣 ) )
19 15 18 syl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) “ 𝑘 ) ⊆ 𝑣 ) )
20 funmpt ⊢ Fun ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ )
21 simplrl ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → 𝑘 ∈ 𝒫 ∪ 𝑆 )
22 21 elpwid ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → 𝑘 ⊆ ∪ 𝑆 )
23 14 simprd ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → 𝑆 ∈ ( TopOn ‘ 𝑌 ) )
24 toponuni ⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝑆 )
25 23 24 syl ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → 𝑌 = ∪ 𝑆 )
26 22 25 sseqtrrd ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → 𝑘 ⊆ 𝑌 )
27 26 adantr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) → 𝑘 ⊆ 𝑌 )
28 dmmptg ⊢ ( ∀ 𝑦 ∈ 𝑌 ⟨ 𝑦 , 𝑥 ⟩ ∈ V → dom ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = 𝑌 )
29 opex ⊢ ⟨ 𝑦 , 𝑥 ⟩ ∈ V
30 29 a1i ⊢ ( 𝑦 ∈ 𝑌 → ⟨ 𝑦 , 𝑥 ⟩ ∈ V )
31 28 30 mprg ⊢ dom ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = 𝑌
32 27 31 sseqtrrdi ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) → 𝑘 ⊆ dom ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) )
33 funimass4 ⊢ ( ( Fun ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∧ 𝑘 ⊆ dom ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) → ( ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) “ 𝑘 ) ⊆ 𝑣 ↔ ∀ 𝑧 ∈ 𝑘 ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ‘ 𝑧 ) ∈ 𝑣 ) )
34 20 32 33 sylancr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) “ 𝑘 ) ⊆ 𝑣 ↔ ∀ 𝑧 ∈ 𝑘 ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ‘ 𝑧 ) ∈ 𝑣 ) )
35 27 sselda ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑘 ) → 𝑧 ∈ 𝑌 )
36 opeq1 ⊢ ( 𝑦 = 𝑧 → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑧 , 𝑥 ⟩ )
37 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ )
38 opex ⊢ ⟨ 𝑧 , 𝑥 ⟩ ∈ V
39 36 37 38 fvmpt ⊢ ( 𝑧 ∈ 𝑌 → ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ‘ 𝑧 ) = ⟨ 𝑧 , 𝑥 ⟩ )
40 35 39 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑘 ) → ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ‘ 𝑧 ) = ⟨ 𝑧 , 𝑥 ⟩ )
41 40 eleq1d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑘 ) → ( ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ‘ 𝑧 ) ∈ 𝑣 ↔ ⟨ 𝑧 , 𝑥 ⟩ ∈ 𝑣 ) )
42 vex ⊢ 𝑥 ∈ V
43 opeq2 ⊢ ( 𝑤 = 𝑥 → ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑥 ⟩ )
44 43 eleq1d ⊢ ( 𝑤 = 𝑥 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑣 ↔ ⟨ 𝑧 , 𝑥 ⟩ ∈ 𝑣 ) )
45 42 44 ralsn ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑣 ↔ ⟨ 𝑧 , 𝑥 ⟩ ∈ 𝑣 )
46 41 45 bitr4di ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑘 ) → ( ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ‘ 𝑧 ) ∈ 𝑣 ↔ ∀ 𝑤 ∈ { 𝑥 } ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑣 ) )
47 46 ralbidva ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑧 ∈ 𝑘 ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ‘ 𝑧 ) ∈ 𝑣 ↔ ∀ 𝑧 ∈ 𝑘 ∀ 𝑤 ∈ { 𝑥 } ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑣 ) )
48 dfss3 ⊢ ( ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ↔ ∀ 𝑡 ∈ ( 𝑘 × { 𝑥 } ) 𝑡 ∈ 𝑣 )
49 eleq1 ⊢ ( 𝑡 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑡 ∈ 𝑣 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑣 ) )
50 49 ralxp ⊢ ( ∀ 𝑡 ∈ ( 𝑘 × { 𝑥 } ) 𝑡 ∈ 𝑣 ↔ ∀ 𝑧 ∈ 𝑘 ∀ 𝑤 ∈ { 𝑥 } ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑣 )
51 48 50 bitri ⊢ ( ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ↔ ∀ 𝑧 ∈ 𝑘 ∀ 𝑤 ∈ { 𝑥 } ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑣 )
52 47 51 bitr4di ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑧 ∈ 𝑘 ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ‘ 𝑧 ) ∈ 𝑣 ↔ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ) )
53 19 34 52 3bitrd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ) )
54 53 rabbidva ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → { 𝑥 ∈ 𝑋 ∣ ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } = { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } )
55 sneq ⊢ ( 𝑥 = 𝑤 → { 𝑥 } = { 𝑤 } )
56 55 xpeq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑘 × { 𝑥 } ) = ( 𝑘 × { 𝑤 } ) )
57 56 sseq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ↔ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) )
58 57 elrab ⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) )
59 eqid ⊢ ∪ ( 𝑆 ↾t 𝑘 ) = ∪ ( 𝑆 ↾t 𝑘 )
60 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
61 simplr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑆 ↾t 𝑘 ) ∈ Comp )
62 simpll ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
63 62 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
64 topontop ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑅 ∈ Top )
65 63 64 syl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑅 ∈ Top )
66 topontop ⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑆 ∈ Top )
67 66 adantl ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝑆 ∈ Top )
68 64 adantr ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝑅 ∈ Top )
69 txtop ⊢ ( ( 𝑆 ∈ Top ∧ 𝑅 ∈ Top ) → ( 𝑆 ×t 𝑅 ) ∈ Top )
70 67 68 69 syl2anc ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑆 ×t 𝑅 ) ∈ Top )
71 70 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑆 ×t 𝑅 ) ∈ Top )
72 vex ⊢ 𝑘 ∈ V
73 toponmax ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝑅 )
74 63 73 syl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑋 ∈ 𝑅 )
75 xpexg ⊢ ( ( 𝑘 ∈ V ∧ 𝑋 ∈ 𝑅 ) → ( 𝑘 × 𝑋 ) ∈ V )
76 72 74 75 sylancr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑘 × 𝑋 ) ∈ V )
77 simprr ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) → 𝑣 ∈ ( 𝑆 ×t 𝑅 ) )
78 77 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑣 ∈ ( 𝑆 ×t 𝑅 ) )
79 elrestr ⊢ ( ( ( 𝑆 ×t 𝑅 ) ∈ Top ∧ ( 𝑘 × 𝑋 ) ∈ V ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) → ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ∈ ( ( 𝑆 ×t 𝑅 ) ↾t ( 𝑘 × 𝑋 ) ) )
80 71 76 78 79 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ∈ ( ( 𝑆 ×t 𝑅 ) ↾t ( 𝑘 × 𝑋 ) ) )
81 67 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑆 ∈ Top )
82 72 a1i ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑘 ∈ V )
83 txrest ⊢ ( ( ( 𝑆 ∈ Top ∧ 𝑅 ∈ Top ) ∧ ( 𝑘 ∈ V ∧ 𝑋 ∈ 𝑅 ) ) → ( ( 𝑆 ×t 𝑅 ) ↾t ( 𝑘 × 𝑋 ) ) = ( ( 𝑆 ↾t 𝑘 ) ×t ( 𝑅 ↾t 𝑋 ) ) )
84 81 65 82 74 83 syl22anc ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( ( 𝑆 ×t 𝑅 ) ↾t ( 𝑘 × 𝑋 ) ) = ( ( 𝑆 ↾t 𝑘 ) ×t ( 𝑅 ↾t 𝑋 ) ) )
85 toponuni ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝑅 )
86 63 85 syl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑋 = ∪ 𝑅 )
87 86 oveq2d ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑅 ↾t 𝑋 ) = ( 𝑅 ↾t ∪ 𝑅 ) )
88 60 restid ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑅 ↾t ∪ 𝑅 ) = 𝑅 )
89 63 88 syl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑅 ↾t ∪ 𝑅 ) = 𝑅 )
90 87 89 eqtrd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑅 ↾t 𝑋 ) = 𝑅 )
91 90 oveq2d ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( ( 𝑆 ↾t 𝑘 ) ×t ( 𝑅 ↾t 𝑋 ) ) = ( ( 𝑆 ↾t 𝑘 ) ×t 𝑅 ) )
92 84 91 eqtrd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( ( 𝑆 ×t 𝑅 ) ↾t ( 𝑘 × 𝑋 ) ) = ( ( 𝑆 ↾t 𝑘 ) ×t 𝑅 ) )
93 80 92 eleqtrd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ∈ ( ( 𝑆 ↾t 𝑘 ) ×t 𝑅 ) )
94 23 adantr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑆 ∈ ( TopOn ‘ 𝑌 ) )
95 26 adantr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑘 ⊆ 𝑌 )
96 resttopon ⊢ ( ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑘 ⊆ 𝑌 ) → ( 𝑆 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
97 94 95 96 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑆 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
98 toponuni ⊢ ( ( 𝑆 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) → 𝑘 = ∪ ( 𝑆 ↾t 𝑘 ) )
99 97 98 syl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑘 = ∪ ( 𝑆 ↾t 𝑘 ) )
100 99 xpeq1d ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑘 × { 𝑤 } ) = ( ∪ ( 𝑆 ↾t 𝑘 ) × { 𝑤 } ) )
101 simprr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 )
102 simprl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑤 ∈ 𝑋 )
103 102 snssd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → { 𝑤 } ⊆ 𝑋 )
104 xpss2 ⊢ ( { 𝑤 } ⊆ 𝑋 → ( 𝑘 × { 𝑤 } ) ⊆ ( 𝑘 × 𝑋 ) )
105 103 104 syl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑘 × { 𝑤 } ) ⊆ ( 𝑘 × 𝑋 ) )
106 101 105 ssind ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( 𝑘 × { 𝑤 } ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) )
107 100 106 eqsstrrd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( ∪ ( 𝑆 ↾t 𝑘 ) × { 𝑤 } ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) )
108 102 86 eleqtrd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → 𝑤 ∈ ∪ 𝑅 )
109 59 60 61 65 93 107 108 txtube ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ∃ 𝑟 ∈ 𝑅 ( 𝑤 ∈ 𝑟 ∧ ( ∪ ( 𝑆 ↾t 𝑘 ) × 𝑟 ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ) )
110 toponss ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑟 ∈ 𝑅 ) → 𝑟 ⊆ 𝑋 )
111 63 110 sylan ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑟 ⊆ 𝑋 )
112 ssrab ⊢ ( 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ↔ ( 𝑟 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ) )
113 112 baib ⊢ ( 𝑟 ⊆ 𝑋 → ( 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ↔ ∀ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ) )
114 111 113 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ↔ ∀ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ) )
115 xpss2 ⊢ ( 𝑟 ⊆ 𝑋 → ( 𝑘 × 𝑟 ) ⊆ ( 𝑘 × 𝑋 ) )
116 111 115 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( 𝑘 × 𝑟 ) ⊆ ( 𝑘 × 𝑋 ) )
117 116 biantrud ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( 𝑘 × 𝑟 ) ⊆ 𝑣 ↔ ( ( 𝑘 × 𝑟 ) ⊆ 𝑣 ∧ ( 𝑘 × 𝑟 ) ⊆ ( 𝑘 × 𝑋 ) ) ) )
118 iunid ⊢ ∪ 𝑥 ∈ 𝑟 { 𝑥 } = 𝑟
119 118 xpeq2i ⊢ ( 𝑘 × ∪ 𝑥 ∈ 𝑟 { 𝑥 } ) = ( 𝑘 × 𝑟 )
120 xpiundi ⊢ ( 𝑘 × ∪ 𝑥 ∈ 𝑟 { 𝑥 } ) = ∪ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } )
121 119 120 eqtr3i ⊢ ( 𝑘 × 𝑟 ) = ∪ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } )
122 121 sseq1i ⊢ ( ( 𝑘 × 𝑟 ) ⊆ 𝑣 ↔ ∪ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 )
123 iunss ⊢ ( ∪ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ↔ ∀ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 )
124 122 123 bitri ⊢ ( ( 𝑘 × 𝑟 ) ⊆ 𝑣 ↔ ∀ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 )
125 ssin ⊢ ( ( ( 𝑘 × 𝑟 ) ⊆ 𝑣 ∧ ( 𝑘 × 𝑟 ) ⊆ ( 𝑘 × 𝑋 ) ) ↔ ( 𝑘 × 𝑟 ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) )
126 117 124 125 3bitr3g ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ∀ 𝑥 ∈ 𝑟 ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 ↔ ( 𝑘 × 𝑟 ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ) )
127 99 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑘 = ∪ ( 𝑆 ↾t 𝑘 ) )
128 127 xpeq1d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( 𝑘 × 𝑟 ) = ( ∪ ( 𝑆 ↾t 𝑘 ) × 𝑟 ) )
129 128 sseq1d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( 𝑘 × 𝑟 ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ↔ ( ∪ ( 𝑆 ↾t 𝑘 ) × 𝑟 ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ) )
130 114 126 129 3bitrd ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ↔ ( ∪ ( 𝑆 ↾t 𝑘 ) × 𝑟 ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ) )
131 130 anbi2d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( 𝑤 ∈ 𝑟 ∧ 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ) ↔ ( 𝑤 ∈ 𝑟 ∧ ( ∪ ( 𝑆 ↾t 𝑘 ) × 𝑟 ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ) ) )
132 131 rexbidva ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ( ∃ 𝑟 ∈ 𝑅 ( 𝑤 ∈ 𝑟 ∧ 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ) ↔ ∃ 𝑟 ∈ 𝑅 ( 𝑤 ∈ 𝑟 ∧ ( ∪ ( 𝑆 ↾t 𝑘 ) × 𝑟 ) ⊆ ( 𝑣 ∩ ( 𝑘 × 𝑋 ) ) ) ) )
133 109 132 mpbird ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑘 × { 𝑤 } ) ⊆ 𝑣 ) ) → ∃ 𝑟 ∈ 𝑅 ( 𝑤 ∈ 𝑟 ∧ 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ) )
134 58 133 sylan2b ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑤 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ) → ∃ 𝑟 ∈ 𝑅 ( 𝑤 ∈ 𝑟 ∧ 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ) )
135 134 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → ∀ 𝑤 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ∃ 𝑟 ∈ 𝑅 ( 𝑤 ∈ 𝑟 ∧ 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ) )
136 eltop2 ⊢ ( 𝑅 ∈ Top → ( { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ∈ 𝑅 ↔ ∀ 𝑤 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ∃ 𝑟 ∈ 𝑅 ( 𝑤 ∈ 𝑟 ∧ 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ) ) )
137 14 68 136 3syl ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → ( { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ∈ 𝑅 ↔ ∀ 𝑤 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ∃ 𝑟 ∈ 𝑅 ( 𝑤 ∈ 𝑟 ∧ 𝑟 ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ) ) )
138 135 137 mpbird ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → { 𝑥 ∈ 𝑋 ∣ ( 𝑘 × { 𝑥 } ) ⊆ 𝑣 } ∈ 𝑅 )
139 54 138 eqeltrd ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → { 𝑥 ∈ 𝑋 ∣ ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } ∈ 𝑅 )
140 imaeq2 ⊢ ( 𝑧 = { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( ◡ 𝐹 “ 𝑧 ) = ( ◡ 𝐹 “ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
141 1 mptpreima ⊢ ( ◡ 𝐹 “ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑥 ∈ 𝑋 ∣ ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } }
142 140 141 eqtrdi ⊢ ( 𝑧 = { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( ◡ 𝐹 “ 𝑧 ) = { 𝑥 ∈ 𝑋 ∣ ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } )
143 142 eleq1d ⊢ ( 𝑧 = { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( ( ◡ 𝐹 “ 𝑧 ) ∈ 𝑅 ↔ { 𝑥 ∈ 𝑋 ∣ ( 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } ∈ 𝑅 ) )
144 139 143 syl5ibrcom ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → ( 𝑧 = { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( ◡ 𝐹 “ 𝑧 ) ∈ 𝑅 ) )
145 144 expimpd ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ) ) → ( ( ( 𝑆 ↾t 𝑘 ) ∈ Comp ∧ 𝑧 = { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ 𝐹 “ 𝑧 ) ∈ 𝑅 ) )
146 145 rexlimdvva ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( ∃ 𝑘 ∈ 𝒫 ∪ 𝑆 ∃ 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ( ( 𝑆 ↾t 𝑘 ) ∈ Comp ∧ 𝑧 = { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ 𝐹 “ 𝑧 ) ∈ 𝑅 ) )
147 13 146 biimtrid ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑧 ∈ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ 𝐹 “ 𝑧 ) ∈ 𝑅 ) )
148 147 ralrimiv ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ∀ 𝑧 ∈ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ 𝑅 )
149 simpl ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
150 ovex ⊢ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∈ V
151 150 pwex ⊢ 𝒫 ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∈ V
152 9 10 11 xkotf ⊢ ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } × ( 𝑆 ×t 𝑅 ) ) ⟶ 𝒫 ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) )
153 frn ⊢ ( ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } × ( 𝑆 ×t 𝑅 ) ) ⟶ 𝒫 ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) → ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) )
154 152 153 ax-mp ⊢ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) )
155 151 154 ssexi ⊢ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ∈ V
156 155 a1i ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ∈ V )
157 9 10 11 xkoval ⊢ ( ( 𝑆 ∈ Top ∧ ( 𝑆 ×t 𝑅 ) ∈ Top ) → ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
158 67 70 157 syl2anc ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
159 eqid ⊢ ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 ) = ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 )
160 159 xkotopon ⊢ ( ( 𝑆 ∈ Top ∧ ( 𝑆 ×t 𝑅 ) ∈ Top ) → ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 ) ∈ ( TopOn ‘ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ) )
161 67 70 160 syl2anc ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 ) ∈ ( TopOn ‘ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ) )
162 149 156 158 161 subbascn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑅 Cn ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 ) ) ↔ ( 𝐹 : 𝑋 ⟶ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑘 ∈ { 𝑤 ∈ 𝒫 ∪ 𝑆 ∣ ( 𝑆 ↾t 𝑤 ) ∈ Comp } , 𝑣 ∈ ( 𝑆 ×t 𝑅 ) ↦ { 𝑓 ∈ ( 𝑆 Cn ( 𝑆 ×t 𝑅 ) ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ 𝑅 ) ) )
163 8 148 162 mpbir2and ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐹 ∈ ( 𝑅 Cn ( ( 𝑆 ×t 𝑅 ) ↑ko 𝑆 ) ) )