This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtr2id 
 |-  ( 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 )