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

Metamath Proof Explorer

Definition df-tmd

Description: Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Assertion df-tmd TopMnd = { 𝑓 ∈ ( Mnd ∩ TopSp ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctmd ⊢ TopMnd
1 vf ⊢ 𝑓
2 cmnd ⊢ Mnd
3 ctps ⊢ TopSp
4 2 3 cin ⊢ ( Mnd ∩ TopSp )
5 ctopn ⊢ TopOpen
6 1 cv ⊢ 𝑓
7 6 5 cfv ⊢ ( TopOpen ‘ 𝑓 )
8 vj ⊢ 𝑗
9 cplusf ⊢ +𝑓
10 6 9 cfv ⊢ ( +𝑓 ‘ 𝑓 )
11 8 cv ⊢ 𝑗
12 ctx ⊢ ×t
13 11 11 12 co ⊢ ( 𝑗 ×t 𝑗 )
14 ccn ⊢ Cn
15 13 11 14 co ⊢ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 )
16 10 15 wcel ⊢ ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 )
17 16 8 7 wsbc ⊢ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 )
18 17 1 4 crab ⊢ { 𝑓 ∈ ( Mnd ∩ TopSp ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) }
19 0 18 wceq ⊢ TopMnd = { 𝑓 ∈ ( Mnd ∩ TopSp ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) }