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 )