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	|- X = ran G
Assertion	opidon2OLD	|- ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )

Proof

Step	Hyp	Ref	Expression
1		opidon2OLD.1	|- X = ran G
2		eqid	|- dom dom G = dom dom G
3	2	opidonOLD	|- ( G e. ( Magma i^i ExId ) -> G : ( dom dom G X. dom dom G ) -onto-> dom dom G )
4		forn	|- ( G : ( dom dom G X. dom dom G ) -onto-> dom dom G -> ran G = dom dom G )
5	1 4	syl5req	|- ( G : ( dom dom G X. dom dom G ) -onto-> dom dom G -> dom dom G = X )
6		xpeq12	|- ( ( dom dom G = X /\ dom dom G = X ) -> ( dom dom G X. dom dom G ) = ( X X. X ) )
7	6	anidms	|- ( dom dom G = X -> ( dom dom G X. dom dom G ) = ( X X. X ) )
8		foeq2	|- ( ( dom dom G X. dom dom G ) = ( X X. X ) -> ( G : ( dom dom G X. dom dom G ) -onto-> dom dom G <-> G : ( X X. X ) -onto-> dom dom G ) )
9	7 8	syl	|- ( dom dom G = X -> ( G : ( dom dom G X. dom dom G ) -onto-> dom dom G <-> G : ( X X. X ) -onto-> dom dom G ) )
10		foeq3	|- ( dom dom G = X -> ( G : ( X X. X ) -onto-> dom dom G <-> G : ( X X. X ) -onto-> X ) )
11	9 10	bitrd	|- ( dom dom G = X -> ( G : ( dom dom G X. dom dom G ) -onto-> dom dom G <-> G : ( X X. X ) -onto-> X ) )
12	11	biimpd	|- ( dom dom G = X -> ( G : ( dom dom G X. dom dom G ) -onto-> dom dom G -> G : ( X X. X ) -onto-> X ) )
13	5 12	mpcom	|- ( G : ( dom dom G X. dom dom G ) -onto-> dom dom G -> G : ( X X. X ) -onto-> X )
14	3 13	syl	|- ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )