Description: The predicate "is a monoid". (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ismndo2.1 | |
|
Assertion | ismndo2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismndo2.1 | |
|
2 | mndomgmid | |
|
3 | rngopidOLD | |
|
4 | 2 3 | syl | |
5 | 1 4 | eqtrid | |
6 | 5 | a1i | |
7 | fdm | |
|
8 | 7 | dmeqd | |
9 | dmxpid | |
|
10 | 8 9 | eqtr2di | |
11 | 10 | 3ad2ant1 | |
12 | 11 | a1i | |
13 | eqid | |
|
14 | 13 | ismndo1 | |
15 | xpid11 | |
|
16 | 15 | biimpri | |
17 | feq23 | |
|
18 | 16 17 | mpancom | |
19 | raleq | |
|
20 | 19 | raleqbi1dv | |
21 | 20 | raleqbi1dv | |
22 | raleq | |
|
23 | 22 | rexeqbi1dv | |
24 | 18 21 23 | 3anbi123d | |
25 | 24 | bibi2d | |
26 | 14 25 | syl5ibrcom | |
27 | 6 12 26 | pm5.21ndd | |