Description: Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | issubm.b | |
|
issubm.z | |
||
issubm.p | |
||
Assertion | issubm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issubm.b | |
|
2 | issubm.z | |
|
3 | issubm.p | |
|
4 | fveq2 | |
|
5 | 4 | pweqd | |
6 | fveq2 | |
|
7 | 6 | eleq1d | |
8 | fveq2 | |
|
9 | 8 | oveqd | |
10 | 9 | eleq1d | |
11 | 10 | 2ralbidv | |
12 | 7 11 | anbi12d | |
13 | 5 12 | rabeqbidv | |
14 | df-submnd | |
|
15 | fvex | |
|
16 | 15 | pwex | |
17 | 16 | rabex | |
18 | 13 14 17 | fvmpt | |
19 | 18 | eleq2d | |
20 | eleq2 | |
|
21 | eleq2 | |
|
22 | 21 | raleqbi1dv | |
23 | 22 | raleqbi1dv | |
24 | 20 23 | anbi12d | |
25 | 24 | elrab | |
26 | 1 | sseq2i | |
27 | 2 | eleq1i | |
28 | 3 | oveqi | |
29 | 28 | eleq1i | |
30 | 29 | 2ralbii | |
31 | 27 30 | anbi12i | |
32 | 26 31 | anbi12i | |
33 | 3anass | |
|
34 | 15 | elpw2 | |
35 | 34 | anbi1i | |
36 | 32 33 35 | 3bitr4ri | |
37 | 25 36 | bitri | |
38 | 19 37 | bitrdi | |