Metamath Proof Explorer

Theorem prdstmdd

Description: The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses prdstmdd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdstmdd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdstmdd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdstmdd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ TopMnd )
Assertion prdstmdd ( 𝜑 → 𝑌 ∈ TopMnd )

Proof

Step Hyp Ref Expression
1 prdstmdd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdstmdd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3 prdstmdd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prdstmdd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ TopMnd )
5 tmdmnd ⊢ ( 𝑥 ∈ TopMnd → 𝑥 ∈ Mnd )
6 5 ssriv ⊢ TopMnd ⊆ Mnd
7 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ TopMnd ∧ TopMnd ⊆ Mnd ) → 𝑅 : 𝐼 ⟶ Mnd )
8 4 6 7 sylancl ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
9 1 2 3 8 prdsmndd ⊢ ( 𝜑 → 𝑌 ∈ Mnd )
10 tmdtps ⊢ ( 𝑥 ∈ TopMnd → 𝑥 ∈ TopSp )
11 10 ssriv ⊢ TopMnd ⊆ TopSp
12 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ TopMnd ∧ TopMnd ⊆ TopSp ) → 𝑅 : 𝐼 ⟶ TopSp )
13 4 11 12 sylancl ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ TopSp )
14 1 3 2 13 prdstps ⊢ ( 𝜑 → 𝑌 ∈ TopSp )
15 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
16 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝑆 ∈ 𝑉 )
17 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝐼 ∈ 𝑊 )
18 4 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
19 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝑅 Fn 𝐼 )
20 simp2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝑓 ∈ ( Base ‘ 𝑌 ) )
21 simp3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝑔 ∈ ( Base ‘ 𝑌 ) )
22 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
23 1 15 16 17 19 20 21 22 prdsplusgval ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑓 ( +g ‘ 𝑌 ) 𝑔 ) = ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( 𝑔 ‘ 𝑘 ) ) ) )
24 23 mpoeq3dva ⊢ ( 𝜑 → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑓 ( +g ‘ 𝑌 ) 𝑔 ) ) = ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( 𝑔 ‘ 𝑘 ) ) ) ) )
25 eqid ⊢ ( +𝑓 ‘ 𝑌 ) = ( +𝑓 ‘ 𝑌 )
26 15 22 25 plusffval ⊢ ( +𝑓 ‘ 𝑌 ) = ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑓 ( +g ‘ 𝑌 ) 𝑔 ) )
27 vex ⊢ 𝑓 ∈ V
28 vex ⊢ 𝑔 ∈ V
29 27 28 op1std ⊢ ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( 1st ‘ 𝑧 ) = 𝑓 )
30 29 fveq1d ⊢ ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( ( 1st ‘ 𝑧 ) ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
31 27 28 op2ndd ⊢ ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑔 )
32 31 fveq1d ⊢ ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( ( 2nd ‘ 𝑧 ) ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
33 30 32 oveq12d ⊢ ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( ( ( 1st ‘ 𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( ( 2nd ‘ 𝑧 ) ‘ 𝑘 ) ) = ( ( 𝑓 ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( 𝑔 ‘ 𝑘 ) ) )
34 33 mpteq2dv ⊢ ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 1st ‘ 𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( ( 2nd ‘ 𝑧 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( 𝑔 ‘ 𝑘 ) ) ) )
35 34 mpompt ⊢ ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑘 ∈ 𝐼 ↦ ( ( ( 1st ‘ 𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( ( 2nd ‘ 𝑧 ) ‘ 𝑘 ) ) ) ) = ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( 𝑔 ‘ 𝑘 ) ) ) )
36 24 26 35 3eqtr4g ⊢ ( 𝜑 → ( +𝑓 ‘ 𝑌 ) = ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑘 ∈ 𝐼 ↦ ( ( ( 1st ‘ 𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( ( 2nd ‘ 𝑧 ) ‘ 𝑘 ) ) ) ) )
37 eqid ⊢ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) )
38 eqid ⊢ ( TopOpen ‘ 𝑌 ) = ( TopOpen ‘ 𝑌 )
39 15 38 istps ⊢ ( 𝑌 ∈ TopSp ↔ ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
40 14 39 sylib ⊢ ( 𝜑 → ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
41 txtopon ⊢ ( ( ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) ∧ ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) ) → ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) ∈ ( TopOn ‘ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) )
42 40 40 41 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) ∈ ( TopOn ‘ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) )
43 topnfn ⊢ TopOpen Fn V
44 ssv ⊢ TopSp ⊆ V
45 fnssres ⊢ ( ( TopOpen Fn V ∧ TopSp ⊆ V ) → ( TopOpen ↾ TopSp ) Fn TopSp )
46 43 44 45 mp2an ⊢ ( TopOpen ↾ TopSp ) Fn TopSp
47 fvres ⊢ ( 𝑥 ∈ TopSp → ( ( TopOpen ↾ TopSp ) ‘ 𝑥 ) = ( TopOpen ‘ 𝑥 ) )
48 eqid ⊢ ( TopOpen ‘ 𝑥 ) = ( TopOpen ‘ 𝑥 )
49 48 tpstop ⊢ ( 𝑥 ∈ TopSp → ( TopOpen ‘ 𝑥 ) ∈ Top )
50 47 49 eqeltrd ⊢ ( 𝑥 ∈ TopSp → ( ( TopOpen ↾ TopSp ) ‘ 𝑥 ) ∈ Top )
51 50 rgen ⊢ ∀ 𝑥 ∈ TopSp ( ( TopOpen ↾ TopSp ) ‘ 𝑥 ) ∈ Top
52 ffnfv ⊢ ( ( TopOpen ↾ TopSp ) : TopSp ⟶ Top ↔ ( ( TopOpen ↾ TopSp ) Fn TopSp ∧ ∀ 𝑥 ∈ TopSp ( ( TopOpen ↾ TopSp ) ‘ 𝑥 ) ∈ Top ) )
53 46 51 52 mpbir2an ⊢ ( TopOpen ↾ TopSp ) : TopSp ⟶ Top
54 fco2 ⊢ ( ( ( TopOpen ↾ TopSp ) : TopSp ⟶ Top ∧ 𝑅 : 𝐼 ⟶ TopSp ) → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
55 53 13 54 sylancr ⊢ ( 𝜑 → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
56 33 mpompt ⊢ ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st ‘ 𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( ( 2nd ‘ 𝑧 ) ‘ 𝑘 ) ) ) = ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( ( 𝑓 ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( 𝑔 ‘ 𝑘 ) ) )
57 eqid ⊢ ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) )
58 eqid ⊢ ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑘 ) )
59 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ TopMnd )
60 40 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
61 60 60 cnmpt1st ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ 𝑓 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) )
62 1 3 2 18 38 prdstopn ⊢ ( 𝜑 → ( TopOpen ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( TopOpen ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
64 63 60 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
65 toponuni ⊢ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) → ( Base ‘ 𝑌 ) = ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
66 64 65 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( Base ‘ 𝑌 ) = ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
67 66 mpteq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥 ‘ 𝑘 ) ) = ( 𝑥 ∈ ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥 ‘ 𝑘 ) ) )
68 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
69 55 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
70 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
71 eqid ⊢ ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) )
72 71 37 ptpjcn ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
73 68 69 70 72 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
74 67 73 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
75 63 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( TopOpen ‘ 𝑌 ) )
76 fvco3 ⊢ ( ( 𝑅 : 𝐼 ⟶ TopMnd ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) )
77 4 76 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) )
78 75 77 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) = ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
79 74 78 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥 ‘ 𝑘 ) ) ∈ ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
80 fveq1 ⊢ ( 𝑥 = 𝑓 → ( 𝑥 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
81 60 60 61 60 79 80 cnmpt21 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
82 60 60 cnmpt2nd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ 𝑔 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) )
83 fveq1 ⊢ ( 𝑥 = 𝑔 → ( 𝑥 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
84 60 60 82 60 79 83 cnmpt21 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑔 ‘ 𝑘 ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
85 57 58 59 60 60 81 84 cnmpt2plusg ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( ( 𝑓 ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( 𝑔 ‘ 𝑘 ) ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
86 77 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) = ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
87 85 86 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( ( 𝑓 ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( 𝑔 ‘ 𝑘 ) ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
88 56 87 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st ‘ 𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( ( 2nd ‘ 𝑧 ) ‘ 𝑘 ) ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
89 37 42 2 55 88 ptcn ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑘 ∈ 𝐼 ↦ ( ( ( 1st ‘ 𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅 ‘ 𝑘 ) ) ( ( 2nd ‘ 𝑧 ) ‘ 𝑘 ) ) ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) )
90 36 89 eqeltrd ⊢ ( 𝜑 → ( +𝑓 ‘ 𝑌 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) )
91 62 oveq2d ⊢ ( 𝜑 → ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) = ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) )
92 90 91 eleqtrrd ⊢ ( 𝜑 → ( +𝑓 ‘ 𝑌 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) )
93 25 38 istmd ⊢ ( 𝑌 ∈ TopMnd ↔ ( 𝑌 ∈ Mnd ∧ 𝑌 ∈ TopSp ∧ ( +𝑓 ‘ 𝑌 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) ) )
94 9 14 92 93 syl3anbrc ⊢ ( 𝜑 → 𝑌 ∈ TopMnd )