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

Metamath Proof Explorer

Theorem rngopidOLD

Description: Obsolete version of mndpfo as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	rngopidOLD	$⊢ G \in (Magma \cap ExId) \to ran G = dom dom G$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ dom dom G = dom dom G$
2	1	opidonOLD	$⊢ G \in (Magma \cap ExId) \to G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G$
3		forn	$⊢ G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G \to ran G = dom dom G$
4	2 3	syl	$⊢ G \in (Magma \cap ExId) \to ran G = dom dom G$