Metamath Proof Explorer


Theorem op0le

Description: Orthoposet zero is less than or equal to any element. ( ch0le analog.) (Contributed by NM, 12-Oct-2011)

Ref Expression
Hypotheses op0le.b B = Base K
op0le.l ˙ = K
op0le.z 0 ˙ = 0. K
Assertion op0le K OP X B 0 ˙ ˙ X

Proof

Step Hyp Ref Expression
1 op0le.b B = Base K
2 op0le.l ˙ = K
3 op0le.z 0 ˙ = 0. K
4 eqid glb K = glb K
5 simpl K OP X B K OP
6 simpr K OP X B X B
7 eqid lub K = lub K
8 1 7 4 op01dm K OP B dom lub K B dom glb K
9 8 simprd K OP B dom glb K
10 9 adantr K OP X B B dom glb K
11 1 4 2 3 5 6 10 p0le K OP X B 0 ˙ ˙ X