Metamath Proof Explorer

Definition df-ghomOLD

Description: Obsolete version of df-ghm 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.)

Ref Expression
Assertion df-ghomOLD ⊢ GrpOpHom = g ∈ GrpOp , h ∈ GrpOp ⟼ f | f : ran ⁡ g ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cghomOLD class GrpOpHom
1 vg setvar g
2 cgr class GrpOp
3 vh setvar h
4 vf setvar f
5 4 cv setvar f
6 1 cv setvar g
7 6 crn class ran ⁡ g
8 3 cv setvar h
9 8 crn class ran ⁡ h
10 7 9 5 wf wff f : ran ⁡ g ⟶ ran ⁡ h
11 vx setvar x
12 vy setvar y
13 11 cv setvar x
14 13 5 cfv class f ⁡ x
15 12 cv setvar y
16 15 5 cfv class f ⁡ y
17 14 16 8 co class f ⁡ x h f ⁡ y
18 13 15 6 co class x g y
19 18 5 cfv class f ⁡ x g y
20 17 19 wceq wff f ⁡ x h f ⁡ y = f ⁡ x g y
21 20 12 7 wral wff ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y
22 21 11 7 wral wff ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y
23 10 22 wa wff f : ran ⁡ g ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y
24 23 4 cab class f | f : ran ⁡ g ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y
25 1 3 2 2 24 cmpo class g ∈ GrpOp , h ∈ GrpOp ⟼ f | f : ran ⁡ g ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y
26 0 25 wceq wff GrpOpHom = g ∈ GrpOp , h ∈ GrpOp ⟼ f | f : ran ⁡ g ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y