Definition df-bj-topmgmhom 38141

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.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-bj-topmgmhom

Step	Hyp	Ref	Expression
1		ctopmgmhom 38140	. 2 class ⎯⎯⎯⎯⟶TopMgm
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		ctmd 24394	. . 3 class TopMnd
5	2	cv 1568	. . . . 5 class 𝑥
6	3	cv 1568	. . . . 5 class 𝑦
7		ctophom 38136	. . . . 5 class ⟶Top
8	5, 6, 7	co 7420	. . . 4 class (𝑥 ⟶Top 𝑦)
9		cmgmhom 38138	. . . . 5 class ⎯⎯⟶Mgm
10	5, 6, 9	co 7420	. . . 4 class (𝑥 ⎯⎯⟶Mgm 𝑦)
11	8, 10	cin 4089	. . 3 class ((𝑥 ⟶Top 𝑦) ∩ (𝑥 ⎯⎯⟶Mgm 𝑦))
12	2, 3, 4, 4, 11	cmpo 7422	. 2 class (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 ⟶Top 𝑦) ∩ (𝑥 ⎯⎯⟶Mgm 𝑦)))
13	1, 12	wceq 1569	1 wff ⎯⎯⎯⎯⟶TopMgm = (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 ⟶Top 𝑦) ∩ (𝑥 ⎯⎯⟶Mgm 𝑦)))

This definition is used by: (None)