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