Definition df-ghomOLD 33683

Description: Obsolete version of df-ghm 17658 as of 15-Mar-2020. Define the set of group homomorphisms from g to h. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-ghomOLD	|- GrpOpHom = ( g e. GrpOp , h e. GrpOp |-> { f | ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) } )

Distinct variable group:   f, g, h, x, y

Detailed syntax breakdown of Definition df-ghomOLD

Step	Hyp	Ref	Expression
1		cghomOLD 33682	. 2 class GrpOpHom
2		vg	. . 3 setvar g
3		vh	. . 3 setvar h
4		cgr 27343	. . 3 class GrpOp
5	2	cv 1482	. . . . . . 7 class g
6	5	crn 5115	. . . . . 6 class ran g
7	3	cv 1482	. . . . . . 7 class h
8	7	crn 5115	. . . . . 6 class ran h
9		vf	. . . . . . 7 setvar f
10	9	cv 1482	. . . . . 6 class f
11	6, 8, 10	wf 5884	. . . . 5 wff f : ran g --> ran h
12		vx	. . . . . . . . . . 11 setvar x
13	12	cv 1482	. . . . . . . . . 10 class x
14	13, 10	cfv 5888	. . . . . . . . 9 class ( f ` x )
15		vy	. . . . . . . . . . 11 setvar y
16	15	cv 1482	. . . . . . . . . 10 class y
17	16, 10	cfv 5888	. . . . . . . . 9 class ( f ` y )
18	14, 17, 7	co 6650	. . . . . . . 8 class ( ( f ` x ) h ( f ` y ) )
19	13, 16, 5	co 6650	. . . . . . . . 9 class ( x g y )
20	19, 10	cfv 5888	. . . . . . . 8 class ( f ` ( x g y ) )
21	18, 20	wceq 1483	. . . . . . 7 wff ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) )
22	21, 15, 6	wral 2912	. . . . . 6 wff A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) )
23	22, 12, 6	wral 2912	. . . . 5 wff A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) )
24	11, 23	wa 384	. . . 4 wff ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) )
25	24, 9	cab 2608	. . 3 class { f | ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) }
26	2, 3, 4, 4, 25	cmpt2 6652	. 2 class ( g e. GrpOp , h e. GrpOp |-> { f | ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) } )
27	1, 26	wceq 1483	1 wff GrpOpHom = ( g e. GrpOp , h e. GrpOp |-> { f | ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) } )

This definition is referenced by:  elghomlem1OLD  33684