Metamath Proof Explorer

Theorem grporndm

Description: A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

Ref Expression
Assertion grporndm 
|- ( G e. GrpOp -> ran G = dom dom G )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran G = ran G
2 1 grpofo 
 |-  ( G e. GrpOp -> G : ( ran G X. ran G ) -onto-> ran G )
3 fof 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> G : ( ran G X. ran G ) --> ran G )
4 3 fdmd 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> dom G = ( ran G X. ran G ) )
5 4 dmeqd 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> dom dom G = dom ( ran G X. ran G ) )
6 dmxpid 
 |-  dom ( ran G X. ran G ) = ran G
7 5 6 eqtr2di 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> ran G = dom dom G )
8 2 7 syl 
 |-  ( G e. GrpOp -> ran G = dom dom G )