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 = f ∈ Mnd ∩ TopSp | [˙ TopOpen ⁡ f / j]˙ + 𝑓 ⁡ f ∈ j × t j Cn j

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctmd class TopMnd
1 vf setvar f
2 cmnd class Mnd
3 ctps class TopSp
4 2 3 cin class Mnd ∩ TopSp
5 ctopn class TopOpen
6 1 cv setvar f
7 6 5 cfv class TopOpen ⁡ f
8 vj setvar j
9 cplusf class + 𝑓
10 6 9 cfv class + 𝑓 ⁡ f
11 8 cv setvar j
12 ctx class × t
13 11 11 12 co class j × t j
14 ccn class Cn
15 13 11 14 co class j × t j Cn j
16 10 15 wcel wff + 𝑓 ⁡ f ∈ j × t j Cn j
17 16 8 7 wsbc wff [˙ TopOpen ⁡ f / j]˙ + 𝑓 ⁡ f ∈ j × t j Cn j
18 17 1 4 crab class f ∈ Mnd ∩ TopSp | [˙ TopOpen ⁡ f / j]˙ + 𝑓 ⁡ f ∈ j × t j Cn j
19 0 18 wceq wff TopMnd = f ∈ Mnd ∩ TopSp | [˙ TopOpen ⁡ f / j]˙ + 𝑓 ⁡ f ∈ j × t j Cn j