Description: The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismgmid.b | |
|
ismgmid.o | |
||
ismgmid.p | |
||
mgmidcl.e | |
||
Assertion | ismgmid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismgmid.b | |
|
2 | ismgmid.o | |
|
3 | ismgmid.p | |
|
4 | mgmidcl.e | |
|
5 | id | |
|
6 | mgmidmo | |
|
7 | reu5 | |
|
8 | 4 6 7 | sylanblrc | |
9 | oveq1 | |
|
10 | 9 | eqeq1d | |
11 | 10 | ovanraleqv | |
12 | 11 | riota2 | |
13 | 5 8 12 | syl2anr | |
14 | 13 | pm5.32da | |
15 | riotacl | |
|
16 | 8 15 | syl | |
17 | eleq1 | |
|
18 | 16 17 | syl5ibcom | |
19 | 18 | pm4.71rd | |
20 | df-riota | |
|
21 | 1 3 2 | grpidval | |
22 | 20 21 | eqtr4i | |
23 | 22 | eqeq1i | |
24 | 23 | a1i | |
25 | 14 19 24 | 3bitr2d | |