Metamath Proof Explorer

Theorem opidonOLD

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) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis opidonOLD.1 
|- X = dom dom G
Assertion opidonOLD 
|- ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )

Proof

Step Hyp Ref Expression
1 opidonOLD.1 
 |-  X = dom dom G
2 inss1 
 |-  ( Magma i^i ExId ) C_ Magma
3 2 sseli 
 |-  ( G e. ( Magma i^i ExId ) -> G e. Magma )
4 1 ismgmOLD 
 |-  ( G e. Magma -> ( G e. Magma <-> G : ( X X. X ) --> X ) )
5 4 ibi 
 |-  ( G e. Magma -> G : ( X X. X ) --> X )
6 3 5 syl 
 |-  ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) --> X )
7 inss2 
 |-  ( Magma i^i ExId ) C_ ExId
8 7 sseli 
 |-  ( G e. ( Magma i^i ExId ) -> G e. ExId )
9 1 isexid 
 |-  ( G e. ExId -> ( G e. ExId <-> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
10 9 biimpd 
 |-  ( G e. ExId -> ( G e. ExId -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
11 8 8 10 sylc 
 |-  ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
12 simpl 
 |-  ( ( ( u G x ) = x /\ ( x G u ) = x ) -> ( u G x ) = x )
13 12 ralimi 
 |-  ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X ( u G x ) = x )
14 oveq2 
 |-  ( x = y -> ( u G x ) = ( u G y ) )
15 id 
 |-  ( x = y -> x = y )
16 14 15 eqeq12d 
 |-  ( x = y -> ( ( u G x ) = x <-> ( u G y ) = y ) )
17 16 rspcv 
 |-  ( y e. X -> ( A. x e. X ( u G x ) = x -> ( u G y ) = y ) )
18 eqcom 
 |-  ( y = ( u G x ) <-> ( u G x ) = y )
19 14 eqeq1d 
 |-  ( x = y -> ( ( u G x ) = y <-> ( u G y ) = y ) )
20 18 19 bitrid 
 |-  ( x = y -> ( y = ( u G x ) <-> ( u G y ) = y ) )
21 20 rspcev 
 |-  ( ( y e. X /\ ( u G y ) = y ) -> E. x e. X y = ( u G x ) )
22 21 ex 
 |-  ( y e. X -> ( ( u G y ) = y -> E. x e. X y = ( u G x ) ) )
23 17 22 syld 
 |-  ( y e. X -> ( A. x e. X ( u G x ) = x -> E. x e. X y = ( u G x ) ) )
24 13 23 syl5 
 |-  ( y e. X -> ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> E. x e. X y = ( u G x ) ) )
25 24 reximdv 
 |-  ( y e. X -> ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> E. u e. X E. x e. X y = ( u G x ) ) )
26 25 impcom 
 |-  ( ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ y e. X ) -> E. u e. X E. x e. X y = ( u G x ) )
27 26 ralrimiva 
 |-  ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. y e. X E. u e. X E. x e. X y = ( u G x ) )
28 11 27 syl 
 |-  ( G e. ( Magma i^i ExId ) -> A. y e. X E. u e. X E. x e. X y = ( u G x ) )
29 foov 
 |-  ( G : ( X X. X ) -onto-> X <-> ( G : ( X X. X ) --> X /\ A. y e. X E. u e. X E. x e. X y = ( u G x ) ) )
30 6 28 29 sylanbrc 
 |-  ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )