Metamath Proof Explorer


Definition df-bj-topmgmhom

Description: Define the set of topological magma morphisms (continuous magma morphisms) between two topological magmas. If domain and codomain are topological semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. This definition is currently stated with topological monoid domain and codomain, since topological magmas are currently not defined in set.mm. (Contributed by BJ, 10-Feb-2022)

Ref Expression
Assertion df-bj-topmgmhom TopMgm⟶ = ( 𝑥 ∈ TopMnd , 𝑦 ∈ TopMnd ↦ ( ( 𝑥 Top𝑦 ) ∩ ( 𝑥 Mgm𝑦 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctopmgmhom TopMgm
1 vx 𝑥
2 ctmd TopMnd
3 vy 𝑦
4 1 cv 𝑥
5 ctophom Top
6 3 cv 𝑦
7 4 6 5 co ( 𝑥 Top𝑦 )
8 cmgmhom Mgm
9 4 6 8 co ( 𝑥 Mgm𝑦 )
10 7 9 cin ( ( 𝑥 Top𝑦 ) ∩ ( 𝑥 Mgm𝑦 ) )
11 1 3 2 2 10 cmpo ( 𝑥 ∈ TopMnd , 𝑦 ∈ TopMnd ↦ ( ( 𝑥 Top𝑦 ) ∩ ( 𝑥 Mgm𝑦 ) ) )
12 0 11 wceq TopMgm⟶ = ( 𝑥 ∈ TopMnd , 𝑦 ∈ TopMnd ↦ ( ( 𝑥 Top𝑦 ) ∩ ( 𝑥 Mgm𝑦 ) ) )