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 GrpOp ran G = dom dom G

Proof

Step Hyp Ref Expression
1 eqid ran G = ran G
2 1 grpofo G GrpOp G : ran G × ran G onto ran G
3 fof G : ran G × ran G onto ran G G : ran G × ran G ran G
4 3 fdmd G : ran G × ran G onto ran G dom G = ran G × ran G
5 4 dmeqd G : ran G × ran G onto ran G dom dom G = dom ran G × ran G
6 dmxpid dom ran G × ran G = ran G
7 5 6 eqtr2di G : ran G × ran G onto ran G ran G = dom dom G
8 2 7 syl G GrpOp ran G = dom dom G