grporndm

Description: A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

		Ref	Expression
	Assertion	grporndm	$⊢ G \in GrpOp \to ran G = dom dom G$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran G = ran G$
2	1	grpofo	$⊢ G \in GrpOp \to G : ran G \times ran G \underset{onto}{⟶} ran G$
3		fof	$⊢ G : ran G \times ran G \underset{onto}{⟶} ran G \to G : ran G \times ran G ⟶ ran G$
4	3	fdmd	$⊢ G : ran G \times ran G \underset{onto}{⟶} ran G \to dom G = ran G \times ran G$
5	4	dmeqd	$⊢ G : ran G \times ran G \underset{onto}{⟶} ran G \to dom dom G = dom (ran G \times ran G)$
6		dmxpid	$⊢ dom (ran G \times ran G) = ran G$
7	5 6	eqtr2di	$⊢ G : ran G \times ran G \underset{onto}{⟶} ran G \to ran G = dom dom G$
8	2 7	syl	$⊢ G \in GrpOp \to ran G = dom dom G$

Metamath Proof Explorer