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 \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \mathrm{ran}G=\mathrm{dom}\mathrm{dom}G$$

Proof

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