Metamath Proof Explorer

Theorem xkopt

Description: The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion xkopt ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝑅 ↑ko 𝒫 𝐴 ) = ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )

Proof

Step Hyp Ref Expression
1 distop ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )
2 simpl ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → 𝑅 ∈ Top )
3 unipw ⊢ ∪ 𝒫 𝐴 = 𝐴
4 3 eqcomi ⊢ 𝐴 = ∪ 𝒫 𝐴
5 eqid ⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp }
6 eqid ⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
7 4 5 6 xkoval ⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top ) → ( 𝑅 ↑ko 𝒫 𝐴 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
8 1 2 7 syl2an2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝑅 ↑ko 𝒫 𝐴 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
9 simpr ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
10 fconst6g ⊢ ( 𝑅 ∈ Top → ( 𝐴 × { 𝑅 } ) : 𝐴 ⟶ Top )
11 10 adantr ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 × { 𝑅 } ) : 𝐴 ⟶ Top )
12 pttop ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐴 × { 𝑅 } ) : 𝐴 ⟶ Top ) → ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ∈ Top )
13 9 11 12 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ∈ Top )
14 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
15 restdis ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝒫 𝐴 ↾t 𝑥 ) = 𝒫 𝑥 )
16 14 15 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝒫 𝐴 ↾t 𝑥 ) = 𝒫 𝑥 )
17 16 adantll ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝒫 𝐴 ↾t 𝑥 ) = 𝒫 𝑥 )
18 17 eleq1d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp ↔ 𝒫 𝑥 ∈ Comp ) )
19 discmp ⊢ ( 𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Comp )
20 18 19 bitr4di ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp ↔ 𝑥 ∈ Fin ) )
21 20 rabbidva ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } = { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin } )
22 dfin5 ⊢ ( 𝒫 𝐴 ∩ Fin ) = { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin }
23 21 22 eqtr4di ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } = ( 𝒫 𝐴 ∩ Fin ) )
24 eqidd ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = 𝑅 )
25 toptopon2 ⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) )
26 cndis ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) ) → ( 𝒫 𝐴 Cn 𝑅 ) = ( ∪ 𝑅 ↑m 𝐴 ) )
27 26 ancoms ⊢ ( ( 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝒫 𝐴 Cn 𝑅 ) = ( ∪ 𝑅 ↑m 𝐴 ) )
28 25 27 sylanb ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝒫 𝐴 Cn 𝑅 ) = ( ∪ 𝑅 ↑m 𝐴 ) )
29 28 rabeqdv ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } = { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
30 23 24 29 mpoeq123dv ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
31 30 rneqd ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ran ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
32 eqid ⊢ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
33 32 rnmpo ⊢ ran ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑥 ∣ ∃ 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑣 ∈ 𝑅 𝑥 = { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } }
34 31 33 eqtrdi ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑥 ∣ ∃ 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑣 ∈ 𝑅 𝑥 = { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } )
35 elmapi ⊢ ( 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ ∪ 𝑅 )
36 eleq2 ⊢ ( 𝑣 = if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ↔ ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) )
37 36 imbi2d ⊢ ( 𝑣 = if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) ) )
38 37 bibi1d ⊢ ( 𝑣 = if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) → ( ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ↔ ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ) ↔ ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ) ) )
39 eleq2 ⊢ ( ∪ 𝑅 = if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑅 ↔ ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) )
40 39 imbi2d ⊢ ( ∪ 𝑅 = if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑅 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) ) )
41 40 bibi1d ⊢ ( ∪ 𝑅 = if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) → ( ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑅 ) ↔ ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ) ↔ ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ) ) )
42 simprl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) )
43 42 elin1d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → 𝑘 ∈ 𝒫 𝐴 )
44 43 elpwid ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → 𝑘 ⊆ 𝐴 )
45 44 adantr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → 𝑘 ⊆ 𝐴 )
46 45 sselda ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) → 𝑥 ∈ 𝐴 )
47 simpr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) → 𝑥 ∈ 𝑘 )
48 46 47 2thd ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝑘 ) )
49 48 imbi1d ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ↔ ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ) )
50 ffvelcdm ⊢ ( ( 𝑓 : 𝐴 ⟶ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑅 )
51 50 ex ⊢ ( 𝑓 : 𝐴 ⟶ ∪ 𝑅 → ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑅 ) )
52 51 adantl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑅 ) )
53 52 adantr ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) ∧ ¬ 𝑥 ∈ 𝑘 ) → ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑅 ) )
54 pm2.21 ⊢ ( ¬ 𝑥 ∈ 𝑘 → ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) )
55 54 adantl ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) ∧ ¬ 𝑥 ∈ 𝑘 ) → ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) )
56 53 55 2thd ⊢ ( ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) ∧ ¬ 𝑥 ∈ 𝑘 ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑅 ) ↔ ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ) )
57 38 41 49 56 ifbothda ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑘 → ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) ) )
58 57 ralbidv2 ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝑘 ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) )
59 ffn ⊢ ( 𝑓 : 𝐴 ⟶ ∪ 𝑅 → 𝑓 Fn 𝐴 )
60 59 adantl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → 𝑓 Fn 𝐴 )
61 vex ⊢ 𝑓 ∈ V
62 61 elixp ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) )
63 62 baib ⊢ ( 𝑓 Fn 𝐴 → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) )
64 60 63 syl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) )
65 ffun ⊢ ( 𝑓 : 𝐴 ⟶ ∪ 𝑅 → Fun 𝑓 )
66 fdm ⊢ ( 𝑓 : 𝐴 ⟶ ∪ 𝑅 → dom 𝑓 = 𝐴 )
67 66 adantl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → dom 𝑓 = 𝐴 )
68 45 67 sseqtrrd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → 𝑘 ⊆ dom 𝑓 )
69 funimass4 ⊢ ( ( Fun 𝑓 ∧ 𝑘 ⊆ dom 𝑓 ) → ( ( 𝑓 “ 𝑘 ) ⊆ 𝑣 ↔ ∀ 𝑥 ∈ 𝑘 ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) )
70 65 68 69 syl2an2 ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → ( ( 𝑓 “ 𝑘 ) ⊆ 𝑣 ↔ ∀ 𝑥 ∈ 𝑘 ( 𝑓 ‘ 𝑥 ) ∈ 𝑣 ) )
71 58 64 70 3bitr4d ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 : 𝐴 ⟶ ∪ 𝑅 ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ↔ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 ) )
72 35 71 sylan2 ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ↔ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 ) )
73 72 rabbi2dva ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → ( ( ∪ 𝑅 ↑m 𝐴 ) ∩ X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) = { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
74 elssuni ⊢ ( 𝑣 ∈ 𝑅 → 𝑣 ⊆ ∪ 𝑅 )
75 74 ad2antll ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → 𝑣 ⊆ ∪ 𝑅 )
76 ssid ⊢ ∪ 𝑅 ⊆ ∪ 𝑅
77 sseq1 ⊢ ( 𝑣 = if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) → ( 𝑣 ⊆ ∪ 𝑅 ↔ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ ∪ 𝑅 ) )
78 sseq1 ⊢ ( ∪ 𝑅 = if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) → ( ∪ 𝑅 ⊆ ∪ 𝑅 ↔ if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ ∪ 𝑅 ) )
79 77 78 ifboth ⊢ ( ( 𝑣 ⊆ ∪ 𝑅 ∧ ∪ 𝑅 ⊆ ∪ 𝑅 ) → if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ ∪ 𝑅 )
80 75 76 79 sylancl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ ∪ 𝑅 )
81 80 ralrimivw ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → ∀ 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ ∪ 𝑅 )
82 ss2ixp ⊢ ( ∀ 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ ∪ 𝑅 → X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ X 𝑥 ∈ 𝐴 ∪ 𝑅 )
83 81 82 syl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ X 𝑥 ∈ 𝐴 ∪ 𝑅 )
84 simplr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → 𝐴 ∈ 𝑉 )
85 uniexg ⊢ ( 𝑅 ∈ Top → ∪ 𝑅 ∈ V )
86 85 ad2antrr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → ∪ 𝑅 ∈ V )
87 ixpconstg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑅 ∈ V ) → X 𝑥 ∈ 𝐴 ∪ 𝑅 = ( ∪ 𝑅 ↑m 𝐴 ) )
88 84 86 87 syl2anc ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → X 𝑥 ∈ 𝐴 ∪ 𝑅 = ( ∪ 𝑅 ↑m 𝐴 ) )
89 83 88 sseqtrd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ ( ∪ 𝑅 ↑m 𝐴 ) )
90 sseqin2 ⊢ ( X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ⊆ ( ∪ 𝑅 ↑m 𝐴 ) ↔ ( ( ∪ 𝑅 ↑m 𝐴 ) ∩ X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) = X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) )
91 89 90 sylib ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → ( ( ∪ 𝑅 ↑m 𝐴 ) ∩ X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ) = X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) )
92 73 91 eqtr3d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } = X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) )
93 10 ad2antrr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → ( 𝐴 × { 𝑅 } ) : 𝐴 ⟶ Top )
94 42 elin2d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → 𝑘 ∈ Fin )
95 simplrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑣 ∈ 𝑅 )
96 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
97 96 topopn ⊢ ( 𝑅 ∈ Top → ∪ 𝑅 ∈ 𝑅 )
98 97 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∪ 𝑅 ∈ 𝑅 )
99 95 98 ifcld ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ∈ 𝑅 )
100 fvconst2g ⊢ ( ( 𝑅 ∈ Top ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
101 100 ad4ant14 ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
102 99 101 eleqtrrd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ∈ ( ( 𝐴 × { 𝑅 } ) ‘ 𝑥 ) )
103 eldifn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝑘 ) → ¬ 𝑥 ∈ 𝑘 )
104 103 iffalsed ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝑘 ) → if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) = ∪ 𝑅 )
105 104 adantl ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑘 ) ) → if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) = ∪ 𝑅 )
106 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝑘 ) → 𝑥 ∈ 𝐴 )
107 106 101 sylan2 ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑘 ) ) → ( ( 𝐴 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
108 107 unieqd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑘 ) ) → ∪ ( ( 𝐴 × { 𝑅 } ) ‘ 𝑥 ) = ∪ 𝑅 )
109 105 108 eqtr4d ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑘 ) ) → if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) = ∪ ( ( 𝐴 × { 𝑅 } ) ‘ 𝑥 ) )
110 84 93 94 102 109 ptopn ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → X 𝑥 ∈ 𝐴 if ( 𝑥 ∈ 𝑘 , 𝑣 , ∪ 𝑅 ) ∈ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
111 92 110 eqeltrd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ∈ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
112 eleq1 ⊢ ( 𝑥 = { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → ( 𝑥 ∈ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ↔ { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ∈ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ) )
113 111 112 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑣 ∈ 𝑅 ) ) → ( 𝑥 = { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → 𝑥 ∈ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ) )
114 113 rexlimdvva ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑣 ∈ 𝑅 𝑥 = { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } → 𝑥 ∈ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ) )
115 114 abssdv ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → { 𝑥 ∣ ∃ 𝑘 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑣 ∈ 𝑅 𝑥 = { 𝑓 ∈ ( ∪ 𝑅 ↑m 𝐴 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } } ⊆ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
116 34 115 eqsstrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
117 tgfiss ⊢ ( ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ∈ Top ∧ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ) → ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) ⊆ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
118 13 116 117 syl2anc ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝒫 𝐴 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑅 ↦ { 𝑓 ∈ ( 𝒫 𝐴 Cn 𝑅 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) ⊆ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
119 8 118 eqsstrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝑅 ↑ko 𝒫 𝐴 ) ⊆ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
120 eqid ⊢ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝑅 } ) )
121 120 96 ptuniconst ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top ) → ( ∪ 𝑅 ↑m 𝐴 ) = ∪ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
122 121 ancoms ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ∪ 𝑅 ↑m 𝐴 ) = ∪ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
123 28 122 eqtrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝒫 𝐴 Cn 𝑅 ) = ∪ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
124 123 oveq2d ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ↾t ( 𝒫 𝐴 Cn 𝑅 ) ) = ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ↾t ∪ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ) )
125 eqid ⊢ ∪ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) = ∪ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) )
126 125 restid ⊢ ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ∈ Top → ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ↾t ∪ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ) = ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
127 13 126 syl ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ↾t ∪ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ) = ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
128 124 127 eqtrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ↾t ( 𝒫 𝐴 Cn 𝑅 ) ) = ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )
129 4 120 xkoptsub ⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top ) → ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ↾t ( 𝒫 𝐴 Cn 𝑅 ) ) ⊆ ( 𝑅 ↑ko 𝒫 𝐴 ) )
130 1 2 129 syl2an2 ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ↾t ( 𝒫 𝐴 Cn 𝑅 ) ) ⊆ ( 𝑅 ↑ko 𝒫 𝐴 ) )
131 128 130 eqsstrrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) ⊆ ( 𝑅 ↑ko 𝒫 𝐴 ) )
132 119 131 eqssd ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝑅 ↑ko 𝒫 𝐴 ) = ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) )