Description: The identity element of a group belongs to the group. (Contributed by NM, 24-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | grpoidval.1 | |- X = ran G |
|
| grpoidval.2 | |- U = ( GId ` G ) |
||
| Assertion | grpoidcl | |- ( G e. GrpOp -> U e. X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpoidval.1 | |- X = ran G |
|
| 2 | grpoidval.2 | |- U = ( GId ` G ) |
|
| 3 | 1 2 | grpoidval | |- ( G e. GrpOp -> U = ( iota_ u e. X A. x e. X ( u G x ) = x ) ) |
| 4 | 1 | grpoideu | |- ( G e. GrpOp -> E! u e. X A. x e. X ( u G x ) = x ) |
| 5 | riotacl | |- ( E! u e. X A. x e. X ( u G x ) = x -> ( iota_ u e. X A. x e. X ( u G x ) = x ) e. X ) |
|
| 6 | 4 5 | syl | |- ( G e. GrpOp -> ( iota_ u e. X A. x e. X ( u G x ) = x ) e. X ) |
| 7 | 3 6 | eqeltrd | |- ( G e. GrpOp -> U e. X ) |