This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- G e. GrpOp
grprn.2 
|- dom G = ( X X. X )
Assertion grporn 
|- X = ran G

Proof

Step Hyp Ref Expression
1 grprn.1 
 |-  G e. GrpOp
2 grprn.2 
 |-  dom G = ( X X. X )
3 eqid 
 |-  ran G = ran G
4 3 grpofo 
 |-  ( G e. GrpOp -> G : ( ran G X. ran G ) -onto-> ran G )
5 fofun 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> Fun G )
6 1 4 5 mp2b 
 |-  Fun G
7 df-fn 
 |-  ( G Fn ( X X. X ) <-> ( Fun G /\ dom G = ( X X. X ) ) )
8 6 2 7 mpbir2an 
 |-  G Fn ( X X. X )
9 fofn 
 |-  ( G : ( ran G X. ran G ) -onto-> ran G -> G Fn ( ran G X. ran G ) )
10 1 4 9 mp2b 
 |-  G Fn ( ran G X. ran G )
11 fndmu 
 |-  ( ( G Fn ( X X. X ) /\ G Fn ( ran G X. ran G ) ) -> ( X X. X ) = ( ran G X. ran G ) )
12 xpid11 
 |-  ( ( X X. X ) = ( ran G X. ran G ) <-> X = ran G )
13 11 12 sylib 
 |-  ( ( G Fn ( X X. X ) /\ G Fn ( ran G X. ran G ) ) -> X = ran G )
14 8 10 13 mp2an 
 |-  X = ran G