Theorem iorlid

Description: A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	iorlid.1	|- X = ran G
	iorlid.2	|- U = ( GId ` G )
Assertion	iorlid	|- ( G e. ( Magma i^i ExId ) -> U e. X )

Proof

Step	Hyp	Ref	Expression
1		iorlid.1	|- X = ran G
2		iorlid.2	|- U = ( GId ` G )
3	1 2	idrval	|- ( G e. ( Magma i^i ExId ) -> U = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
4	1	exidu1	|- ( G e. ( Magma i^i ExId ) -> E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
5		riotacl	|- ( E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) e. X )
6	4 5	syl	|- ( G e. ( Magma i^i ExId ) -> ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) e. X )
7	3 6	eqeltrd	|- ( G e. ( Magma i^i ExId ) -> U e. X )