Description: less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | oppglt.1 | ||
oppglt.2 | |||
Assertion | oppglt |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oppglt.1 | ||
2 | oppglt.2 | ||
3 | eqid | ||
4 | 3 2 | pltfval | |
5 | 1 | fvexi | |
6 | 1 3 | oppgle | |
7 | eqid | ||
8 | 6 7 | pltfval | |
9 | 5 8 | ax-mp | |
10 | 4 9 | eqtr4di |