This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xkoptsub

Description: The compact-open topology is finer than the product topology restricted to continuous functions. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses xkoptsub.x ⊢ 𝑋 = ∪ 𝑅
xkoptsub.j ⊢ 𝐽 = ( ∏t ‘ ( 𝑋 × { 𝑆 } ) )
Assertion xkoptsub ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝐽 ↾t ( 𝑅 Cn 𝑆 ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) )

Proof

Step Hyp Ref Expression
1 xkoptsub.x ⊢ 𝑋 = ∪ 𝑅
2 xkoptsub.j ⊢ 𝐽 = ( ∏t ‘ ( 𝑋 × { 𝑆 } ) )
3 1 topopn ⊢ ( 𝑅 ∈ Top → 𝑋 ∈ 𝑅 )
4 3 adantr ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝑋 ∈ 𝑅 )
5 fconstg ⊢ ( 𝑆 ∈ Top → ( 𝑋 × { 𝑆 } ) : 𝑋 ⟶ { 𝑆 } )
6 5 adantl ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × { 𝑆 } ) : 𝑋 ⟶ { 𝑆 } )
7 6 ffnd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × { 𝑆 } ) Fn 𝑋 )
8 eqid ⊢ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ) }
9 8 ptval ⊢ ( ( 𝑋 ∈ 𝑅 ∧ ( 𝑋 × { 𝑆 } ) Fn 𝑋 ) → ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ) } ) )
10 4 7 9 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ) } ) )
11 simpr ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝑆 ∈ Top )
12 11 snssd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → { 𝑆 } ⊆ Top )
13 6 12 fssd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × { 𝑆 } ) : 𝑋 ⟶ Top )
14 eqid ⊢ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) = X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 )
15 8 14 ptbasfi ⊢ ( ( 𝑋 ∈ 𝑅 ∧ ( 𝑋 × { 𝑆 } ) : 𝑋 ⟶ Top ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ) } = ( fi ‘ ( { X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) )
16 4 13 15 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ) } = ( fi ‘ ( { X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) )
17 fvconst2g ⊢ ( ( 𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋 ) → ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) = 𝑆 )
18 17 adantll ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑛 ∈ 𝑋 ) → ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) = 𝑆 )
19 18 unieqd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑛 ∈ 𝑋 ) → ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) = ∪ 𝑆 )
20 19 ixpeq2dva ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) = X 𝑛 ∈ 𝑋 ∪ 𝑆 )
21 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
22 21 topopn ⊢ ( 𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆 )
23 ixpconstg ⊢ ( ( 𝑋 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆 ) → X 𝑛 ∈ 𝑋 ∪ 𝑆 = ( ∪ 𝑆 ↑m 𝑋 ) )
24 3 22 23 syl2an ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → X 𝑛 ∈ 𝑋 ∪ 𝑆 = ( ∪ 𝑆 ↑m 𝑋 ) )
25 20 24 eqtrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) = ( ∪ 𝑆 ↑m 𝑋 ) )
26 25 sneqd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → { X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) } = { ( ∪ 𝑆 ↑m 𝑋 ) } )
27 eqid ⊢ 𝑋 = 𝑋
28 fvconst2g ⊢ ( ( 𝑆 ∈ Top ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) = 𝑆 )
29 28 adantll ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) = 𝑆 )
30 25 adantr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑘 ∈ 𝑋 ) → X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) = ( ∪ 𝑆 ↑m 𝑋 ) )
31 30 mpteq1d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) )
32 31 cnveqd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑘 ∈ 𝑋 ) → ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) )
33 32 imaeq1d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑘 ∈ 𝑋 ) → ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
34 33 ralrimivw ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑘 ∈ 𝑋 ) → ∀ 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
35 29 34 jca ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) = 𝑆 ∧ ∀ 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
36 35 ralrimiva ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∀ 𝑘 ∈ 𝑋 ( ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) = 𝑆 ∧ ∀ 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
37 mpoeq123 ⊢ ( ( 𝑋 = 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) = 𝑆 ∧ ∀ 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → ( 𝑘 ∈ 𝑋 , 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) = ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
38 27 36 37 sylancr ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑘 ∈ 𝑋 , 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) = ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
39 38 rneqd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) = ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
40 26 39 uneq12d ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( { X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) = ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) )
41 40 fveq2d ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( fi ‘ ( { X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝑋 ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) = ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) )
42 16 41 eqtrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ) } = ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) )
43 42 fveq2d ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝑋 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝑋 × { 𝑆 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝑋 ( 𝑔 ‘ 𝑦 ) ) } ) = ( topGen ‘ ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ) )
44 10 43 eqtrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∏t ‘ ( 𝑋 × { 𝑆 } ) ) = ( topGen ‘ ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ) )
45 2 44 eqtrid ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝐽 = ( topGen ‘ ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ) )
46 45 oveq1d ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝐽 ↾t ( 𝑅 Cn 𝑆 ) ) = ( ( topGen ‘ ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) )
47 firest ⊢ ( fi ‘ ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) = ( ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ↾t ( 𝑅 Cn 𝑆 ) )
48 47 fveq2i ⊢ ( topGen ‘ ( fi ‘ ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) ) = ( topGen ‘ ( ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) )
49 fvex ⊢ ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ∈ V
50 ovex ⊢ ( 𝑅 Cn 𝑆 ) ∈ V
51 tgrest ⊢ ( ( ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ∈ V ∧ ( 𝑅 Cn 𝑆 ) ∈ V ) → ( topGen ‘ ( ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) = ( ( topGen ‘ ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) )
52 49 50 51 mp2an ⊢ ( topGen ‘ ( ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) = ( ( topGen ‘ ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ) ↾t ( 𝑅 Cn 𝑆 ) )
53 48 52 eqtri ⊢ ( topGen ‘ ( fi ‘ ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) ) = ( ( topGen ‘ ( fi ‘ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) ) ↾t ( 𝑅 Cn 𝑆 ) )
54 46 53 eqtr4di ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝐽 ↾t ( 𝑅 Cn 𝑆 ) ) = ( topGen ‘ ( fi ‘ ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) ) )
55 xkotop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ Top )
56 snex ⊢ { ( ∪ 𝑆 ↑m 𝑋 ) } ∈ V
57 mpoexga ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top ) → ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ∈ V )
58 3 57 sylan ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ∈ V )
59 rnexg ⊢ ( ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ∈ V → ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ∈ V )
60 58 59 syl ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ∈ V )
61 unexg ⊢ ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∈ V ∧ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ∈ V ) → ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ∈ V )
62 56 60 61 sylancr ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ∈ V )
63 restval ⊢ ( ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ∈ V ∧ ( 𝑅 Cn 𝑆 ) ∈ V ) → ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) = ran ( 𝑥 ∈ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↦ ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ) )
64 62 50 63 sylancl ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) = ran ( 𝑥 ∈ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↦ ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ) )
65 elun ⊢ ( 𝑥 ∈ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↔ ( 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } ∨ 𝑥 ∈ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) )
66 1 21 cnf ⊢ ( 𝑥 ∈ ( 𝑅 Cn 𝑆 ) → 𝑥 : 𝑋 ⟶ ∪ 𝑆 )
67 elmapg ⊢ ( ( ∪ 𝑆 ∈ 𝑆 ∧ 𝑋 ∈ 𝑅 ) → ( 𝑥 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↔ 𝑥 : 𝑋 ⟶ ∪ 𝑆 ) )
68 22 3 67 syl2anr ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑥 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↔ 𝑥 : 𝑋 ⟶ ∪ 𝑆 ) )
69 66 68 imbitrrid ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑥 ∈ ( 𝑅 Cn 𝑆 ) → 𝑥 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ) )
70 69 ssrdv ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) ⊆ ( ∪ 𝑆 ↑m 𝑋 ) )
71 70 adantr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } ) → ( 𝑅 Cn 𝑆 ) ⊆ ( ∪ 𝑆 ↑m 𝑋 ) )
72 elsni ⊢ ( 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } → 𝑥 = ( ∪ 𝑆 ↑m 𝑋 ) )
73 72 adantl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } ) → 𝑥 = ( ∪ 𝑆 ↑m 𝑋 ) )
74 71 73 sseqtrrd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } ) → ( 𝑅 Cn 𝑆 ) ⊆ 𝑥 )
75 sseqin2 ⊢ ( ( 𝑅 Cn 𝑆 ) ⊆ 𝑥 ↔ ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) = ( 𝑅 Cn 𝑆 ) )
76 74 75 sylib ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) = ( 𝑅 Cn 𝑆 ) )
77 eqid ⊢ ( 𝑆 ↑ko 𝑅 ) = ( 𝑆 ↑ko 𝑅 )
78 77 xkouni ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) = ∪ ( 𝑆 ↑ko 𝑅 ) )
79 eqid ⊢ ∪ ( 𝑆 ↑ko 𝑅 ) = ∪ ( 𝑆 ↑ko 𝑅 )
80 79 topopn ⊢ ( ( 𝑆 ↑ko 𝑅 ) ∈ Top → ∪ ( 𝑆 ↑ko 𝑅 ) ∈ ( 𝑆 ↑ko 𝑅 ) )
81 55 80 syl ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∪ ( 𝑆 ↑ko 𝑅 ) ∈ ( 𝑆 ↑ko 𝑅 ) )
82 78 81 eqeltrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) ∈ ( 𝑆 ↑ko 𝑅 ) )
83 82 adantr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } ) → ( 𝑅 Cn 𝑆 ) ∈ ( 𝑆 ↑ko 𝑅 ) )
84 76 83 eqeltrd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) )
85 eqid ⊢ ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) = ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
86 85 rnmpo ⊢ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) = { 𝑥 ∣ ∃ 𝑘 ∈ 𝑋 ∃ 𝑢 ∈ 𝑆 𝑥 = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) }
87 86 eqabri ⊢ ( 𝑥 ∈ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝑋 ∃ 𝑢 ∈ 𝑆 𝑥 = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
88 cnvresima ⊢ ( ◡ ( ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ↾ ( 𝑅 Cn 𝑆 ) ) “ 𝑢 ) = ( ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∩ ( 𝑅 Cn 𝑆 ) )
89 70 adantr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑅 Cn 𝑆 ) ⊆ ( ∪ 𝑆 ↑m 𝑋 ) )
90 89 resmptd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ↾ ( 𝑅 Cn 𝑆 ) ) = ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) )
91 90 cnveqd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ◡ ( ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ↾ ( 𝑅 Cn 𝑆 ) ) = ◡ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) )
92 91 imaeq1d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( ◡ ( ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ↾ ( 𝑅 Cn 𝑆 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
93 88 92 eqtr3id ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∩ ( 𝑅 Cn 𝑆 ) ) = ( ◡ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
94 fvex ⊢ ( 𝑤 ‘ 𝑘 ) ∈ V
95 94 rgenw ⊢ ∀ 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ( 𝑤 ‘ 𝑘 ) ∈ V
96 eqid ⊢ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) )
97 96 fnmpt ⊢ ( ∀ 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ( 𝑤 ‘ 𝑘 ) ∈ V → ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) Fn ( 𝑅 Cn 𝑆 ) )
98 95 97 mp1i ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) Fn ( 𝑅 Cn 𝑆 ) )
99 elpreima ⊢ ( ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) Fn ( 𝑅 Cn 𝑆 ) → ( 𝑓 ∈ ( ◡ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ↔ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ‘ 𝑓 ) ∈ 𝑢 ) ) )
100 98 99 syl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑓 ∈ ( ◡ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ↔ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ‘ 𝑓 ) ∈ 𝑢 ) ) )
101 fveq1 ⊢ ( 𝑤 = 𝑓 → ( 𝑤 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
102 fvex ⊢ ( 𝑓 ‘ 𝑘 ) ∈ V
103 101 96 102 fvmpt ⊢ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) → ( ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ‘ 𝑓 ) = ( 𝑓 ‘ 𝑘 ) )
104 103 adantl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ‘ 𝑓 ) = ( 𝑓 ‘ 𝑘 ) )
105 104 eleq1d ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ‘ 𝑓 ) ∈ 𝑢 ↔ ( 𝑓 ‘ 𝑘 ) ∈ 𝑢 ) )
106 102 snss ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ 𝑢 ↔ { ( 𝑓 ‘ 𝑘 ) } ⊆ 𝑢 )
107 89 sselda ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝑓 ∈ ( ∪ 𝑆 ↑m 𝑋 ) )
108 elmapi ⊢ ( 𝑓 ∈ ( ∪ 𝑆 ↑m 𝑋 ) → 𝑓 : 𝑋 ⟶ ∪ 𝑆 )
109 ffn ⊢ ( 𝑓 : 𝑋 ⟶ ∪ 𝑆 → 𝑓 Fn 𝑋 )
110 107 108 109 3syl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝑓 Fn 𝑋 )
111 simplrl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → 𝑘 ∈ 𝑋 )
112 fnsnfv ⊢ ( ( 𝑓 Fn 𝑋 ∧ 𝑘 ∈ 𝑋 ) → { ( 𝑓 ‘ 𝑘 ) } = ( 𝑓 “ { 𝑘 } ) )
113 110 111 112 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → { ( 𝑓 ‘ 𝑘 ) } = ( 𝑓 “ { 𝑘 } ) )
114 113 sseq1d ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → ( { ( 𝑓 ‘ 𝑘 ) } ⊆ 𝑢 ↔ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 ) )
115 106 114 bitrid ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( 𝑓 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 ) )
116 105 115 bitrd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → ( ( ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ‘ 𝑓 ) ∈ 𝑢 ↔ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 ) )
117 116 pm5.32da ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ‘ 𝑓 ) ∈ 𝑢 ) ↔ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 ) ) )
118 100 117 bitrd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑓 ∈ ( ◡ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ↔ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 ) ) )
119 118 eqabdv ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( ◡ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = { 𝑓 ∣ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 ) } )
120 df-rab ⊢ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 } = { 𝑓 ∣ ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 ) }
121 119 120 eqtr4di ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( ◡ ( 𝑤 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 } )
122 93 121 eqtrd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∩ ( 𝑅 Cn 𝑆 ) ) = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 } )
123 simpll ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑅 ∈ Top )
124 11 adantr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑆 ∈ Top )
125 simprl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑘 ∈ 𝑋 )
126 125 snssd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → { 𝑘 } ⊆ 𝑋 )
127 1 toptopon ⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
128 123 127 sylib ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
129 restsn2 ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑅 ↾t { 𝑘 } ) = 𝒫 { 𝑘 } )
130 128 125 129 syl2anc ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑅 ↾t { 𝑘 } ) = 𝒫 { 𝑘 } )
131 snfi ⊢ { 𝑘 } ∈ Fin
132 discmp ⊢ ( { 𝑘 } ∈ Fin ↔ 𝒫 { 𝑘 } ∈ Comp )
133 131 132 mpbi ⊢ 𝒫 { 𝑘 } ∈ Comp
134 130 133 eqeltrdi ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑅 ↾t { 𝑘 } ) ∈ Comp )
135 simprr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑢 ∈ 𝑆 )
136 1 123 124 126 134 135 xkoopn ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ { 𝑘 } ) ⊆ 𝑢 } ∈ ( 𝑆 ↑ko 𝑅 ) )
137 122 136 eqeltrd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) )
138 ineq1 ⊢ ( 𝑥 = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) = ( ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∩ ( 𝑅 Cn 𝑆 ) ) )
139 138 eleq1d ⊢ ( 𝑥 = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) ↔ ( ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) ) )
140 137 139 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑥 = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) ) )
141 140 rexlimdvva ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∃ 𝑘 ∈ 𝑋 ∃ 𝑢 ∈ 𝑆 𝑥 = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) ) )
142 141 imp ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ∃ 𝑘 ∈ 𝑋 ∃ 𝑢 ∈ 𝑆 𝑥 = ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) )
143 87 142 sylan2b ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑥 ∈ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) )
144 84 143 jaodan ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑥 ∈ { ( ∪ 𝑆 ↑m 𝑋 ) } ∨ 𝑥 ∈ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) )
145 65 144 sylan2b ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑥 ∈ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) → ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ∈ ( 𝑆 ↑ko 𝑅 ) )
146 145 fmpttd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑥 ∈ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↦ ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ) : ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ⟶ ( 𝑆 ↑ko 𝑅 ) )
147 146 frnd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ran ( 𝑥 ∈ ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↦ ( 𝑥 ∩ ( 𝑅 Cn 𝑆 ) ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) )
148 64 147 eqsstrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) )
149 tgfiss ⊢ ( ( ( 𝑆 ↑ko 𝑅 ) ∈ Top ∧ ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) ) → ( topGen ‘ ( fi ‘ ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) )
150 55 148 149 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( topGen ‘ ( fi ‘ ( ( { ( ∪ 𝑆 ↑m 𝑋 ) } ∪ ran ( 𝑘 ∈ 𝑋 , 𝑢 ∈ 𝑆 ↦ ( ◡ ( 𝑤 ∈ ( ∪ 𝑆 ↑m 𝑋 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ↾t ( 𝑅 Cn 𝑆 ) ) ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) )
151 54 150 eqsstrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝐽 ↾t ( 𝑅 Cn 𝑆 ) ) ⊆ ( 𝑆 ↑ko 𝑅 ) )