Description: Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | oppggic.o | |
|
Assertion | oppgsubm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oppggic.o | |
|
2 | submrcl | |
|
3 | submrcl | |
|
4 | 1 | oppgmndb | |
5 | 3 4 | sylibr | |
6 | ralcom | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | 7 1 8 | oppgplus | |
10 | 9 | eleq1i | |
11 | 10 | 2ralbii | |
12 | 6 11 | bitr4i | |
13 | 12 | 3anbi3i | |
14 | 13 | a1i | |
15 | eqid | |
|
16 | eqid | |
|
17 | 15 16 7 | issubm | |
18 | 1 15 | oppgbas | |
19 | 1 16 | oppgid | |
20 | 18 19 8 | issubm | |
21 | 4 20 | sylbi | |
22 | 14 17 21 | 3bitr4d | |
23 | 2 5 22 | pm5.21nii | |
24 | 23 | eqriv | |