# 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}={\mathrm{Base}}_{{K}}$
op0le.l
op0le.z
Assertion op0le

### Proof

Step Hyp Ref Expression
1 op0le.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 op0le.l
3 op0le.z
4 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
5 simpl ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to {K}\in \mathrm{OP}$
6 simpr ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to {X}\in {B}$
7 eqid ${⊢}\mathrm{lub}\left({K}\right)=\mathrm{lub}\left({K}\right)$
8 1 7 4 op01dm ${⊢}{K}\in \mathrm{OP}\to \left({B}\in \mathrm{dom}\mathrm{lub}\left({K}\right)\wedge {B}\in \mathrm{dom}\mathrm{glb}\left({K}\right)\right)$
9 8 simprd ${⊢}{K}\in \mathrm{OP}\to {B}\in \mathrm{dom}\mathrm{glb}\left({K}\right)$
10 9 adantr ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to {B}\in \mathrm{dom}\mathrm{glb}\left({K}\right)$
11 1 4 2 3 5 6 10 p0le