Definition df-ghomOLD 32853

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

Assertion

Ref	Expression
df-ghomOLD	⊢ GrpOpHom = (𝑔 ∈ GrpOp, ℎ ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))})

Distinct variable group:   𝑓,𝑔,ℎ,𝑥,𝑦

Detailed syntax breakdown of Definition df-ghomOLD

Step	Hyp	Ref	Expression
1		cghomOLD 32852	. 2 class GrpOpHom
2		vg	. . 3 setvar 𝑔
3		vh	. . 3 setvar ℎ
4		cgr 26727	. . 3 class GrpOp
5	2	cv 1474	. . . . . . 7 class 𝑔
6	5	crn 5039	. . . . . 6 class ran 𝑔
7	3	cv 1474	. . . . . . 7 class ℎ
8	7	crn 5039	. . . . . 6 class ran ℎ
9		vf	. . . . . . 7 setvar 𝑓
10	9	cv 1474	. . . . . 6 class 𝑓
11	6, 8, 10	wf 5800	. . . . 5 wff 𝑓:ran 𝑔⟶ran ℎ
12		vx	. . . . . . . . . . 11 setvar 𝑥
13	12	cv 1474	. . . . . . . . . 10 class 𝑥
14	13, 10	cfv 5804	. . . . . . . . 9 class (𝑓‘𝑥)
15		vy	. . . . . . . . . . 11 setvar 𝑦
16	15	cv 1474	. . . . . . . . . 10 class 𝑦
17	16, 10	cfv 5804	. . . . . . . . 9 class (𝑓‘𝑦)
18	14, 17, 7	co 6549	. . . . . . . 8 class ((𝑓‘𝑥)ℎ(𝑓‘𝑦))
19	13, 16, 5	co 6549	. . . . . . . . 9 class (𝑥𝑔𝑦)
20	19, 10	cfv 5804	. . . . . . . 8 class (𝑓‘(𝑥𝑔𝑦))
21	18, 20	wceq 1475	. . . . . . 7 wff ((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦))
22	21, 15, 6	wral 2896	. . . . . 6 wff ∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦))
23	22, 12, 6	wral 2896	. . . . 5 wff ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦))
24	11, 23	wa 383	. . . 4 wff (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))
25	24, 9	cab 2596	. . 3 class {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))}
26	2, 3, 4, 4, 25	cmpt2 6551	. 2 class (𝑔 ∈ GrpOp, ℎ ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))})
27	1, 26	wceq 1475	1 wff GrpOpHom = (𝑔 ∈ GrpOp, ℎ ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))})

This definition is referenced by:  elghomlem1OLD  32854