Metamath Proof Explorer

Theorem xkoccn

Description: The "constant function" function which maps x e. Y to the constant function z e. X |-> x is a continuous function from X into the space of continuous functions from Y to X . This can also be understood as the currying of the first projection function. (The currying of the second projection function is x e. Y |-> ( z e. X |-> z ) , which we already know is continuous because it is a constant function.) (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion xkoccn ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) ∈ ( 𝑆 Cn ( 𝑆 ↑ko 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 cnconst2 ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 × { 𝑥 } ) ∈ ( 𝑅 Cn 𝑆 ) )
2 1 3expa ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 × { 𝑥 } ) ∈ ( 𝑅 Cn 𝑆 ) )
3 2 fmpttd ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) : 𝑌 ⟶ ( 𝑅 Cn 𝑆 ) )
4 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
5 eqid ⊢ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } = { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp }
6 eqid ⊢ ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
7 4 5 6 xkobval ⊢ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑦 ∣ ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) }
8 7 abeq2i ⊢ ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ↔ ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
9 2 ad5ant15 ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 × { 𝑥 } ) ∈ ( 𝑅 Cn 𝑆 ) )
10 simplr ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) ∧ 𝑥 ∈ 𝑌 ) → 𝑘 = ∅ )
11 10 imaeq2d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) = ( ( 𝑋 × { 𝑥 } ) “ ∅ ) )
12 ima0 ⊢ ( ( 𝑋 × { 𝑥 } ) “ ∅ ) = ∅
13 0ss ⊢ ∅ ⊆ 𝑣
14 12 13 eqsstri ⊢ ( ( 𝑋 × { 𝑥 } ) “ ∅ ) ⊆ 𝑣
15 11 14 eqsstrdi ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) ⊆ 𝑣 )
16 imaeq1 ⊢ ( 𝑓 = ( 𝑋 × { 𝑥 } ) → ( 𝑓 “ 𝑘 ) = ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) )
17 16 sseq1d ⊢ ( 𝑓 = ( 𝑋 × { 𝑥 } ) → ( ( 𝑓 “ 𝑘 ) ⊆ 𝑣 ↔ ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) ⊆ 𝑣 ) )
18 17 elrab ⊢ ( ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ ( ( 𝑋 × { 𝑥 } ) ∈ ( 𝑅 Cn 𝑆 ) ∧ ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) ⊆ 𝑣 ) )
19 9 15 18 sylanbrc ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
20 19 ralrimiva ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) → ∀ 𝑥 ∈ 𝑌 ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
21 rabid2 ⊢ ( 𝑌 = { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } ↔ ∀ 𝑥 ∈ 𝑌 ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
22 20 21 sylibr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) → 𝑌 = { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } )
23 simpllr ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑆 ∈ ( TopOn ‘ 𝑌 ) )
24 toponmax ⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝑆 )
25 23 24 syl ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑌 ∈ 𝑆 )
26 25 adantr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) → 𝑌 ∈ 𝑆 )
27 22 26 eqeltrrd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 = ∅ ) → { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } ∈ 𝑆 )
28 ifnefalse ⊢ ( 𝑘 ≠ ∅ → if ( 𝑘 = ∅ , 𝑌 , 𝑣 ) = 𝑣 )
29 28 ad2antlr ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → if ( 𝑘 = ∅ , 𝑌 , 𝑣 ) = 𝑣 )
30 29 eleq2d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ if ( 𝑘 = ∅ , 𝑌 , 𝑣 ) ↔ 𝑥 ∈ 𝑣 ) )
31 vex ⊢ 𝑥 ∈ V
32 31 snss ⊢ ( 𝑥 ∈ 𝑣 ↔ { 𝑥 } ⊆ 𝑣 )
33 30 32 bitrdi ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ if ( 𝑘 = ∅ , 𝑌 , 𝑣 ) ↔ { 𝑥 } ⊆ 𝑣 ) )
34 df-ima ⊢ ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) = ran ( ( 𝑋 × { 𝑥 } ) ↾ 𝑘 )
35 simplrl ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑘 ∈ 𝒫 ∪ 𝑅 )
36 35 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → 𝑘 ∈ 𝒫 ∪ 𝑅 )
37 36 elpwid ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → 𝑘 ⊆ ∪ 𝑅 )
38 toponuni ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝑅 )
39 38 ad5antr ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → 𝑋 = ∪ 𝑅 )
40 37 39 sseqtrrd ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → 𝑘 ⊆ 𝑋 )
41 xpssres ⊢ ( 𝑘 ⊆ 𝑋 → ( ( 𝑋 × { 𝑥 } ) ↾ 𝑘 ) = ( 𝑘 × { 𝑥 } ) )
42 40 41 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑋 × { 𝑥 } ) ↾ 𝑘 ) = ( 𝑘 × { 𝑥 } ) )
43 42 rneqd ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ran ( ( 𝑋 × { 𝑥 } ) ↾ 𝑘 ) = ran ( 𝑘 × { 𝑥 } ) )
44 34 43 syl5eq ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) = ran ( 𝑘 × { 𝑥 } ) )
45 rnxp ⊢ ( 𝑘 ≠ ∅ → ran ( 𝑘 × { 𝑥 } ) = { 𝑥 } )
46 45 ad2antlr ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ran ( 𝑘 × { 𝑥 } ) = { 𝑥 } )
47 44 46 eqtrd ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) = { 𝑥 } )
48 47 sseq1d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) ⊆ 𝑣 ↔ { 𝑥 } ⊆ 𝑣 ) )
49 2 ad5ant15 ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 × { 𝑥 } ) ∈ ( 𝑅 Cn 𝑆 ) )
50 49 biantrurd ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) ⊆ 𝑣 ↔ ( ( 𝑋 × { 𝑥 } ) ∈ ( 𝑅 Cn 𝑆 ) ∧ ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) ⊆ 𝑣 ) ) )
51 33 48 50 3bitr2d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ if ( 𝑘 = ∅ , 𝑌 , 𝑣 ) ↔ ( ( 𝑋 × { 𝑥 } ) ∈ ( 𝑅 Cn 𝑆 ) ∧ ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) ⊆ 𝑣 ) ) )
52 30 51 bitr3d ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ 𝑣 ↔ ( ( 𝑋 × { 𝑥 } ) ∈ ( 𝑅 Cn 𝑆 ) ∧ ( ( 𝑋 × { 𝑥 } ) “ 𝑘 ) ⊆ 𝑣 ) ) )
53 52 18 bitr4di ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ 𝑣 ↔ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
54 53 rabbi2dva ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) → ( 𝑌 ∩ 𝑣 ) = { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } )
55 simplrr ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑣 ∈ 𝑆 )
56 toponss ⊢ ( ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑣 ∈ 𝑆 ) → 𝑣 ⊆ 𝑌 )
57 23 55 56 syl2anc ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → 𝑣 ⊆ 𝑌 )
58 57 adantr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) → 𝑣 ⊆ 𝑌 )
59 sseqin2 ⊢ ( 𝑣 ⊆ 𝑌 ↔ ( 𝑌 ∩ 𝑣 ) = 𝑣 )
60 58 59 sylib ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) → ( 𝑌 ∩ 𝑣 ) = 𝑣 )
61 54 60 eqtr3d ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) → { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } = 𝑣 )
62 55 adantr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) → 𝑣 ∈ 𝑆 )
63 61 62 eqeltrd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) ∧ 𝑘 ≠ ∅ ) → { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } ∈ 𝑆 )
64 27 63 pm2.61dane ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } ∈ 𝑆 )
65 imaeq2 ⊢ ( 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) = ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
66 eqid ⊢ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) )
67 66 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } }
68 65 67 eqtrdi ⊢ ( 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) = { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } )
69 68 eleq1d ⊢ ( 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) ∈ 𝑆 ↔ { 𝑥 ∈ 𝑌 ∣ ( 𝑋 × { 𝑥 } ) ∈ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } ∈ 𝑆 ) )
70 64 69 syl5ibrcom ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) ∧ ( 𝑅 ↾t 𝑘 ) ∈ Comp ) → ( 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) ∈ 𝑆 ) )
71 70 expimpd ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) → ( ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) ∈ 𝑆 ) )
72 71 rexlimdvva ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( ∃ 𝑘 ∈ 𝒫 ∪ 𝑅 ∃ 𝑣 ∈ 𝑆 ( ( 𝑅 ↾t 𝑘 ) ∈ Comp ∧ 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) ∈ 𝑆 ) )
73 8 72 syl5bi ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) → ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) ∈ 𝑆 ) )
74 73 ralrimiv ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ∀ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) ∈ 𝑆 )
75 simpr ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝑆 ∈ ( TopOn ‘ 𝑌 ) )
76 ovex ⊢ ( 𝑅 Cn 𝑆 ) ∈ V
77 76 pwex ⊢ 𝒫 ( 𝑅 Cn 𝑆 ) ∈ V
78 4 5 6 xkotf ⊢ ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 )
79 frn ⊢ ( ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 ) → ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑆 ) )
80 78 79 ax-mp ⊢ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑆 )
81 77 80 ssexi ⊢ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ∈ V
82 81 a1i ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ∈ V )
83 topontop ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑅 ∈ Top )
84 topontop ⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑆 ∈ Top )
85 4 5 6 xkoval ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
86 83 84 85 syl2an ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑆 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
87 eqid ⊢ ( 𝑆 ↑ko 𝑅 ) = ( 𝑆 ↑ko 𝑅 )
88 87 xkotopon ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
89 83 84 88 syl2an ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
90 75 82 86 89 subbascn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) ∈ ( 𝑆 Cn ( 𝑆 ↑ko 𝑅 ) ) ↔ ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) : 𝑌 ⟶ ( 𝑅 Cn 𝑆 ) ∧ ∀ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑧 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑧 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ( ◡ ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) “ 𝑦 ) ∈ 𝑆 ) ) )
91 3 74 90 mpbir2and ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑌 ↦ ( 𝑋 × { 𝑥 } ) ) ∈ ( 𝑆 Cn ( 𝑆 ↑ko 𝑅 ) ) )