Metamath Proof Explorer


Theorem op1le

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 B=BaseK
ople1.l ˙=K
ople1.u 1˙=1.K
Assertion op1le KOPXB1˙˙XX=1˙

Proof

Step Hyp Ref Expression
1 ople1.b B=BaseK
2 ople1.l ˙=K
3 ople1.u 1˙=1.K
4 1 2 3 ople1 KOPXBX˙1˙
5 4 biantrurd KOPXB1˙˙XX˙1˙1˙˙X
6 opposet KOPKPoset
7 6 adantr KOPXBKPoset
8 simpr KOPXBXB
9 1 3 op1cl KOP1˙B
10 9 adantr KOPXB1˙B
11 1 2 posasymb KPosetXB1˙BX˙1˙1˙˙XX=1˙
12 7 8 10 11 syl3anc KOPXBX˙1˙1˙˙XX=1˙
13 5 12 bitrd KOPXB1˙˙XX=1˙