Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-topmgmhom Structured version   Visualization version   GIF version

Definition df-bj-topmgmhom 36005
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
StepHypRef Expression
1 ctopmgmhom 36004 . 2 class TopMgm
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 ctmd 23573 . . 3 class TopMnd
52cv 1540 . . . . 5 class 𝑥
63cv 1540 . . . . 5 class 𝑦
7 ctophom 36000 . . . . 5 class Top
85, 6, 7co 7408 . . . 4 class (𝑥 Top𝑦)
9 cmgmhom 36002 . . . . 5 class Mgm
105, 6, 9co 7408 . . . 4 class (𝑥 Mgm𝑦)
118, 10cin 3947 . . 3 class ((𝑥 Top𝑦) ∩ (𝑥 Mgm𝑦))
122, 3, 4, 4, 11cmpo 7410 . 2 class (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 Top𝑦) ∩ (𝑥 Mgm𝑦)))
131, 12wceq 1541 1 wff TopMgm⟶ = (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 Top𝑦) ∩ (𝑥 Mgm𝑦)))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator