![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-topmgmhom | Structured version Visualization version GIF version |
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 |
---|---|
df-bj-topmgmhom | ⊢ TopMgm⟶ = (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 Top⟶ 𝑦) ∩ (𝑥 Mgm⟶ 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ctopmgmhom 36313 | . 2 class TopMgm⟶ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | ctmd 23795 | . . 3 class TopMnd | |
5 | 2 | cv 1539 | . . . . 5 class 𝑥 |
6 | 3 | cv 1539 | . . . . 5 class 𝑦 |
7 | ctophom 36309 | . . . . 5 class Top⟶ | |
8 | 5, 6, 7 | co 7412 | . . . 4 class (𝑥 Top⟶ 𝑦) |
9 | cmgmhom 36311 | . . . . 5 class Mgm⟶ | |
10 | 5, 6, 9 | co 7412 | . . . 4 class (𝑥 Mgm⟶ 𝑦) |
11 | 8, 10 | cin 3947 | . . 3 class ((𝑥 Top⟶ 𝑦) ∩ (𝑥 Mgm⟶ 𝑦)) |
12 | 2, 3, 4, 4, 11 | cmpo 7414 | . 2 class (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 Top⟶ 𝑦) ∩ (𝑥 Mgm⟶ 𝑦))) |
13 | 1, 12 | wceq 1540 | 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 |