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 e. ( Magma i^i ExId ) -> ran G = dom dom G )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- dom dom G = dom dom G
2	1	opidonOLD	|- ( G e. ( Magma i^i ExId ) -> G : ( dom dom G X. dom dom G ) -onto-> dom dom G )
3		forn	|- ( G : ( dom dom G X. dom dom G ) -onto-> dom dom G -> ran G = dom dom G )
4	2 3	syl	|- ( G e. ( Magma i^i ExId ) -> ran G = dom dom G )