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	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ dom dom 𝐺 = dom dom 𝐺
2	1	opidonOLD	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 )
3		forn	⊢ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → ran 𝐺 = dom dom 𝐺 )
4	2 3	syl	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺 )