Description: Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | issubmnd.b | |
|
issubmnd.p | |
||
issubmnd.z | |
||
issubmnd.h | |
||
Assertion | issubmnd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issubmnd.b | |
|
2 | issubmnd.p | |
|
3 | issubmnd.z | |
|
4 | issubmnd.h | |
|
5 | simplr | |
|
6 | simprl | |
|
7 | simpll2 | |
|
8 | 4 1 | ressbas2 | |
9 | 7 8 | syl | |
10 | 6 9 | eleqtrd | |
11 | simprr | |
|
12 | 11 9 | eleqtrd | |
13 | eqid | |
|
14 | eqid | |
|
15 | 13 14 | mndcl | |
16 | 5 10 12 15 | syl3anc | |
17 | 1 | fvexi | |
18 | 17 | ssex | |
19 | 18 | 3ad2ant2 | |
20 | 4 2 | ressplusg | |
21 | 19 20 | syl | |
22 | 21 | ad2antrr | |
23 | 22 | oveqd | |
24 | 16 23 9 | 3eltr4d | |
25 | 24 | ralrimivva | |
26 | simpl2 | |
|
27 | 26 8 | syl | |
28 | 21 | adantr | |
29 | ovrspc2v | |
|
30 | 29 | ancoms | |
31 | 30 | 3impb | |
32 | 31 | 3adant1l | |
33 | simpl1 | |
|
34 | 26 | sseld | |
35 | 26 | sseld | |
36 | 26 | sseld | |
37 | 34 35 36 | 3anim123d | |
38 | 37 | imp | |
39 | 1 2 | mndass | |
40 | 33 38 39 | syl2an2r | |
41 | simpl3 | |
|
42 | 26 | sselda | |
43 | 1 2 3 | mndlid | |
44 | 33 42 43 | syl2an2r | |
45 | 1 2 3 | mndrid | |
46 | 33 42 45 | syl2an2r | |
47 | 27 28 32 40 41 44 46 | ismndd | |
48 | 25 47 | impbida | |