Description: An atom under a co-atom is strictly less than it. TODO: is this needed? (Contributed by NM, 1-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lhplt.l | |
|
lhplt.s | |
||
lhplt.a | |
||
lhplt.h | |
||
Assertion | lhplt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhplt.l | |
|
2 | lhplt.s | |
|
3 | lhplt.a | |
|
4 | lhplt.h | |
|
5 | simpll | |
|
6 | simprl | |
|
7 | eqid | |
|
8 | 7 4 | lhpbase | |
9 | 8 | ad2antlr | |
10 | eqid | |
|
11 | eqid | |
|
12 | 10 11 4 | lhp1cvr | |
13 | 12 | adantr | |
14 | simprr | |
|
15 | 7 1 2 10 11 3 | 1cvratlt | |
16 | 5 6 9 13 14 15 | syl32anc | |