Description: Property of the set of identities of G . Either G has no identities, and O = (/) , or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mgmidsssn0.b | |
|
mgmidsssn0.z | |
||
mgmidsssn0.p | |
||
mgmidsssn0.o | |
||
Assertion | mgmidsssn0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mgmidsssn0.b | |
|
2 | mgmidsssn0.z | |
|
3 | mgmidsssn0.p | |
|
4 | mgmidsssn0.o | |
|
5 | simpr | |
|
6 | oveq1 | |
|
7 | 6 | eqeq1d | |
8 | 7 | ovanraleqv | |
9 | 8 | rspcev | |
10 | 9 | adantl | |
11 | 1 2 3 10 | ismgmid | |
12 | 5 11 | mpbid | |
13 | 12 | eqcomd | |
14 | velsn | |
|
15 | 13 14 | sylibr | |
16 | 15 | expr | |
17 | 16 | ralrimiva | |
18 | rabss | |
|
19 | 17 18 | sylibr | |
20 | 4 19 | eqsstrid | |