# 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}=\mathrm{ran}{G}$
Assertion grpofo ${⊢}{G}\in \mathrm{GrpOp}\to {G}:{X}×{X}\underset{onto}{⟶}{X}$

### Proof

Step Hyp Ref Expression
1 grpfo.1 ${⊢}{X}=\mathrm{ran}{G}$
2 1 isgrpo ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}\in \mathrm{GrpOp}↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
3 2 ibi ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)$
4 3 simp1d ${⊢}{G}\in \mathrm{GrpOp}\to {G}:{X}×{X}⟶{X}$
5 1 eqcomi ${⊢}\mathrm{ran}{G}={X}$
6 4 5 jctir ${⊢}{G}\in \mathrm{GrpOp}\to \left({G}:{X}×{X}⟶{X}\wedge \mathrm{ran}{G}={X}\right)$
7 dffo2 ${⊢}{G}:{X}×{X}\underset{onto}{⟶}{X}↔\left({G}:{X}×{X}⟶{X}\wedge \mathrm{ran}{G}={X}\right)$
8 6 7 sylibr ${⊢}{G}\in \mathrm{GrpOp}\to {G}:{X}×{X}\underset{onto}{⟶}{X}$