Metamath Proof Explorer


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=ranG
iorlid.2 U=GIdG
Assertion iorlid GMagmaExIdUX

Proof

Step Hyp Ref Expression
1 iorlid.1 X=ranG
2 iorlid.2 U=GIdG
3 1 2 idrval GMagmaExIdU=ιuX|xXuGx=xxGu=x
4 1 exidu1 GMagmaExId∃!uXxXuGx=xxGu=x
5 riotacl ∃!uXxXuGx=xxGu=xιuX|xXuGx=xxGu=xX
6 4 5 syl GMagmaExIdιuX|xXuGx=xxGu=xX
7 3 6 eqeltrd GMagmaExIdUX