Metamath Proof Explorer


Theorem grpofo

Description: A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 X=ranG
Assertion grpofo GGrpOpG:X×XontoX

Proof

Step Hyp Ref Expression
1 grpfo.1 X=ranG
2 1 isgrpo GGrpOpGGrpOpG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
3 2 ibi GGrpOpG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
4 3 simp1d GGrpOpG:X×XX
5 1 eqcomi ranG=X
6 4 5 jctir GGrpOpG:X×XXranG=X
7 dffo2 G:X×XontoXG:X×XXranG=X
8 6 7 sylibr GGrpOpG:X×XontoX