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

Proof

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