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\in \mathrm{GrpOp}$$
	grprn.2	$$⊢\mathrm{dom}G=X\times X$$
Assertion	grporn	$$⊢X=\mathrm{ran}G$$

Proof

Step	Hyp	Ref	Expression
1		grprn.1	$$⊢G\in \mathrm{GrpOp}$$
2		grprn.2	$$⊢\mathrm{dom}G=X\times X$$
3		eqid	$$⊢\mathrm{ran}G=\mathrm{ran}G$$
4	3	grpofo	$$⊢G\in \mathrm{GrpOp}\to G:\mathrm{ran}G\times \mathrm{ran}G\underset{onto}{⟶}\mathrm{ran}G$$
5		fofun	$$⊢G:\mathrm{ran}G\times \mathrm{ran}G\underset{onto}{⟶}\mathrm{ran}G\to \mathrm{Fun}G$$
6	1 4 5	mp2b	$$⊢\mathrm{Fun}G$$
7		df-fn	$$⊢GFn\left(X\times X\right)\leftrightarrow \left(\mathrm{Fun}G\wedge \mathrm{dom}G=X\times X\right)$$
8	6 2 7	mpbir2an	$$⊢GFn\left(X\times X\right)$$
9		fofn	$$⊢G:\mathrm{ran}G\times \mathrm{ran}G\underset{onto}{⟶}\mathrm{ran}G\to GFn\left(\mathrm{ran}G\times \mathrm{ran}G\right)$$
10	1 4 9	mp2b	$$⊢GFn\left(\mathrm{ran}G\times \mathrm{ran}G\right)$$
11		fndmu	$$⊢\left(GFn\left(X\times X\right)\wedge GFn\left(\mathrm{ran}G\times \mathrm{ran}G\right)\right)\to X\times X=\mathrm{ran}G\times \mathrm{ran}G$$
12		xpid11	$$⊢X\times X=\mathrm{ran}G\times \mathrm{ran}G\leftrightarrow X=\mathrm{ran}G$$
13	11 12	sylib	$$⊢\left(GFn\left(X\times X\right)\wedge GFn\left(\mathrm{ran}G\times \mathrm{ran}G\right)\right)\to X=\mathrm{ran}G$$
14	8 10 13	mp2an	$$⊢X=\mathrm{ran}G$$