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

Metamath Proof Explorer

Theorem rngmgmbs4

Description: The range of an internal operation with a left and right identity element equals its base set. (Contributed by FL, 24-Jan-2010) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion rngmgmbs4 
|- ( ( G : ( X X. X ) --> X /\ E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) -> ran G = X )

Proof

Step Hyp Ref Expression
1 r19.12 
 |-  ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X E. u e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
2 simpl 
 |-  ( ( ( u G x ) = x /\ ( x G u ) = x ) -> ( u G x ) = x )
3 2 eqcomd 
 |-  ( ( ( u G x ) = x /\ ( x G u ) = x ) -> x = ( u G x ) )
4 oveq2 
 |-  ( y = x -> ( u G y ) = ( u G x ) )
5 4 rspceeqv 
 |-  ( ( x e. X /\ x = ( u G x ) ) -> E. y e. X x = ( u G y ) )
6 5 ex 
 |-  ( x e. X -> ( x = ( u G x ) -> E. y e. X x = ( u G y ) ) )
7 3 6 syl5 
 |-  ( x e. X -> ( ( ( u G x ) = x /\ ( x G u ) = x ) -> E. y e. X x = ( u G y ) ) )
8 7 reximdv 
 |-  ( x e. X -> ( E. u e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> E. u e. X E. y e. X x = ( u G y ) ) )
9 8 ralimia 
 |-  ( A. x e. X E. u e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X E. u e. X E. y e. X x = ( u G y ) )
10 1 9 syl 
 |-  ( E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X E. u e. X E. y e. X x = ( u G y ) )
11 10 anim2i 
 |-  ( ( G : ( X X. X ) --> X /\ E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) -> ( G : ( X X. X ) --> X /\ A. x e. X E. u e. X E. y e. X x = ( u G y ) ) )
12 foov 
 |-  ( G : ( X X. X ) -onto-> X <-> ( G : ( X X. X ) --> X /\ A. x e. X E. u e. X E. y e. X x = ( u G y ) ) )
13 11 12 sylibr 
 |-  ( ( G : ( X X. X ) --> X /\ E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) -> G : ( X X. X ) -onto-> X )
14 forn 
 |-  ( G : ( X X. X ) -onto-> X -> ran G = X )
15 13 14 syl 
 |-  ( ( G : ( X X. X ) --> X /\ E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) -> ran G = X )