Theorem opidon2OLD

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

	Ref	Expression
Hypothesis	opidon2OLD.1	⊢ 𝑋 = ran 𝐺
Assertion	opidon2OLD	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		opidon2OLD.1	⊢ 𝑋 = ran 𝐺
2		eqid	⊢ dom dom 𝐺 = dom dom 𝐺
3	2	opidonOLD	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 )
4		forn	⊢ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → ran 𝐺 = dom dom 𝐺 )
5	1 4	syl5req	⊢ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → dom dom 𝐺 = 𝑋 )
6		xpeq12	⊢ ( ( dom dom 𝐺 = 𝑋 ∧ dom dom 𝐺 = 𝑋 ) → ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) )
7	6	anidms	⊢ ( dom dom 𝐺 = 𝑋 → ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) )
8		foeq2	⊢ ( ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺 ) )
9	7 8	syl	⊢ ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺 ) )
10		foeq3	⊢ ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) )
11	9 10	bitrd	⊢ ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) )
12	11	biimpd	⊢ ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) )
13	5 12	mpcom	⊢ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )
14	3 13	syl	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )