Description: If the orthoposet unity is less than or equal to an element, the element equals the unit. ( chle0 analog.) (Contributed by NM, 5-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ople1.b | |
|
ople1.l | |
||
ople1.u | |
||
Assertion | op1le | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ople1.b | |
|
2 | ople1.l | |
|
3 | ople1.u | |
|
4 | 1 2 3 | ople1 | |
5 | 4 | biantrurd | |
6 | opposet | |
|
7 | 6 | adantr | |
8 | simpr | |
|
9 | 1 3 | op1cl | |
10 | 9 | adantr | |
11 | 1 2 | posasymb | |
12 | 7 8 10 11 | syl3anc | |
13 | 5 12 | bitrd | |