# 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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ctmd ${class}\mathrm{TopMnd}$
1 vf ${setvar}{f}$
2 cmnd ${class}\mathrm{Mnd}$
3 ctps ${class}\mathrm{TopSp}$
4 2 3 cin ${class}\left(\mathrm{Mnd}\cap \mathrm{TopSp}\right)$
5 ctopn ${class}\mathrm{TopOpen}$
6 1 cv ${setvar}{f}$
7 6 5 cfv ${class}\mathrm{TopOpen}\left({f}\right)$
8 vj ${setvar}{j}$
9 cplusf ${class}{+}_{𝑓}$
10 6 9 cfv ${class}{+}_{𝑓}\left({f}\right)$
11 8 cv ${setvar}{j}$
12 ctx ${class}{×}_{t}$
13 11 11 12 co ${class}\left({j}{×}_{t}{j}\right)$
14 ccn ${class}\mathrm{Cn}$
15 13 11 14 co ${class}\left(\left({j}{×}_{t}{j}\right)\mathrm{Cn}{j}\right)$
16 10 15 wcel ${wff}{+}_{𝑓}\left({f}\right)\in \left(\left({j}{×}_{t}{j}\right)\mathrm{Cn}{j}\right)$
17 16 8 7 wsbc
18 17 1 4 crab
19 0 18 wceq