Description: A non-subgroup-member minus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nelsubginvcld.g | |
|
nelsubginvcld.s | |
||
nelsubginvcld.x | |
||
nelsubginvcld.b | |
||
nelsubgcld.y | |
||
nelsubgsubcld.p | |
||
Assertion | nelsubgsubcld | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nelsubginvcld.g | |
|
2 | nelsubginvcld.s | |
|
3 | nelsubginvcld.x | |
|
4 | nelsubginvcld.b | |
|
5 | nelsubgcld.y | |
|
6 | nelsubgsubcld.p | |
|
7 | 3 | eldifad | |
8 | 4 | subgss | |
9 | 2 8 | syl | |
10 | 9 5 | sseldd | |
11 | eqid | |
|
12 | eqid | |
|
13 | 4 11 12 6 | grpsubval | |
14 | 7 10 13 | syl2anc | |
15 | 12 | subginvcl | |
16 | 2 5 15 | syl2anc | |
17 | 1 2 3 4 16 11 | nelsubgcld | |
18 | 14 17 | eqeltrd | |