Definition df-bj-magmahom 33080

Description: Define the set of magma morphisms between two magmas. (Contributed by BJ, 10-Feb-2022.)

Assertion

Ref	Expression
df-bj-magmahom	|- -Magma-> = ( x e. Mgm , y e. Mgm |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( Base ` x ) A. v e. ( Base ` x ) ( f ` ( u ( +g ` x ) v ) ) = ( ( f ` u ) ( +g ` y ) ( f ` v ) ) } )

Distinct variable group:   x, f, y, u, v

Detailed syntax breakdown of Definition df-bj-magmahom

Step	Hyp	Ref	Expression
1		cmagmahom 33077	. 2 class -Magma->
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cmgm 17240	. . 3 class Mgm
5		vu	. . . . . . . . . 10 setvar u
6	5	cv 1482	. . . . . . . . 9 class u
7		vv	. . . . . . . . . 10 setvar v
8	7	cv 1482	. . . . . . . . 9 class v
9	2	cv 1482	. . . . . . . . . 10 class x
10		cplusg 15941	. . . . . . . . . 10 class +g
11	9, 10	cfv 5888	. . . . . . . . 9 class ( +g ` x )
12	6, 8, 11	co 6650	. . . . . . . 8 class ( u ( +g ` x ) v )
13		vf	. . . . . . . . 9 setvar f
14	13	cv 1482	. . . . . . . 8 class f
15	12, 14	cfv 5888	. . . . . . 7 class ( f ` ( u ( +g ` x ) v ) )
16	6, 14	cfv 5888	. . . . . . . 8 class ( f ` u )
17	8, 14	cfv 5888	. . . . . . . 8 class ( f ` v )
18	3	cv 1482	. . . . . . . . 9 class y
19	18, 10	cfv 5888	. . . . . . . 8 class ( +g ` y )
20	16, 17, 19	co 6650	. . . . . . 7 class ( ( f ` u ) ( +g ` y ) ( f ` v ) )
21	15, 20	wceq 1483	. . . . . 6 wff ( f ` ( u ( +g ` x ) v ) ) = ( ( f ` u ) ( +g ` y ) ( f ` v ) )
22		cbs 15857	. . . . . . 7 class Base
23	9, 22	cfv 5888	. . . . . 6 class ( Base ` x )
24	21, 7, 23	wral 2912	. . . . 5 wff A. v e. ( Base ` x ) ( f ` ( u ( +g ` x ) v ) ) = ( ( f ` u ) ( +g ` y ) ( f ` v ) )
25	24, 5, 23	wral 2912	. . . 4 wff A. u e. ( Base ` x ) A. v e. ( Base ` x ) ( f ` ( u ( +g ` x ) v ) ) = ( ( f ` u ) ( +g ` y ) ( f ` v ) )
26	18, 22	cfv 5888	. . . . 5 class ( Base ` y )
27		csethom 33075	. . . . 5 class -Set->
28	23, 26, 27	co 6650	. . . 4 class ( ( Base ` x ) -Set-> ( Base ` y ) )
29	25, 13, 28	crab 2916	. . 3 class { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( Base ` x ) A. v e. ( Base ` x ) ( f ` ( u ( +g ` x ) v ) ) = ( ( f ` u ) ( +g ` y ) ( f ` v ) ) }
30	2, 3, 4, 4, 29	cmpt2 6652	. 2 class ( x e. Mgm , y e. Mgm |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( Base ` x ) A. v e. ( Base ` x ) ( f ` ( u ( +g ` x ) v ) ) = ( ( f ` u ) ( +g ` y ) ( f ` v ) ) } )
31	1, 30	wceq 1483	1 wff -Magma-> = ( x e. Mgm , y e. Mgm |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( Base ` x ) A. v e. ( Base ` x ) ( f ` ( u ( +g ` x ) v ) ) = ( ( f ` u ) ( +g ` y ) ( f ` v ) ) } )

This definition is referenced by: (None)