Metamath Proof Explorer


Theorem ople1

Description: Any element is less than the orthoposet unit. ( chss analog.) (Contributed by NM, 23-Oct-2011)

Ref Expression
Hypotheses ople1.b B = Base K
ople1.l ˙ = K
ople1.u 1 ˙ = 1. K
Assertion ople1 K OP X B X ˙ 1 ˙

Proof

Step Hyp Ref Expression
1 ople1.b B = Base K
2 ople1.l ˙ = K
3 ople1.u 1 ˙ = 1. K
4 eqid lub K = lub K
5 simpl K OP X B K OP
6 simpr K OP X B X B
7 eqid glb K = glb K
8 1 4 7 op01dm K OP B dom lub K B dom glb K
9 8 simpld K OP B dom lub K
10 9 adantr K OP X B B dom lub K
11 1 4 2 3 5 6 10 ple1 K OP X B X ˙ 1 ˙