Metamath Proof Explorer


Theorem grporn

Description: The range of a group operation. Useful for satisfying group base set hypotheses of the form X = ran G . (Contributed by NM, 5-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grprn.1 GGrpOp
grprn.2 domG=X×X
Assertion grporn X=ranG

Proof

Step Hyp Ref Expression
1 grprn.1 GGrpOp
2 grprn.2 domG=X×X
3 eqid ranG=ranG
4 3 grpofo GGrpOpG:ranG×ranGontoranG
5 fofun G:ranG×ranGontoranGFunG
6 1 4 5 mp2b FunG
7 df-fn GFnX×XFunGdomG=X×X
8 6 2 7 mpbir2an GFnX×X
9 fofn G:ranG×ranGontoranGGFnranG×ranG
10 1 4 9 mp2b GFnranG×ranG
11 fndmu GFnX×XGFnranG×ranGX×X=ranG×ranG
12 xpid11 X×X=ranG×ranGX=ranG
13 11 12 sylib GFnX×XGFnranG×ranGX=ranG
14 8 10 13 mp2an X=ranG