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 = ran G
Assertion grpofo 
|- ( G e. GrpOp -> G : ( X X. X ) -onto-> X )

Proof

Step Hyp Ref Expression
1 grpfo.1 
 |-  X = ran G
2 1 isgrpo 
 |-  ( G e. GrpOp -> ( G e. GrpOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) ) )
3 2 ibi 
 |-  ( G e. GrpOp -> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) )
4 3 simp1d 
 |-  ( G e. GrpOp -> G : ( X X. X ) --> X )
5 1 eqcomi 
 |-  ran G = X
6 4 5 jctir 
 |-  ( G e. GrpOp -> ( G : ( X X. X ) --> X /\ ran G = X ) )
7 dffo2 
 |-  ( G : ( X X. X ) -onto-> X <-> ( G : ( X X. X ) --> X /\ ran G = X ) )
8 6 7 sylibr 
 |-  ( G e. GrpOp -> G : ( X X. X ) -onto-> X )