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

Proof

Step Hyp Ref Expression
1 ople1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 ople1.l
3 ople1.u
4 eqid ${⊢}\mathrm{lub}\left({K}\right)=\mathrm{lub}\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{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
8 1 4 7 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 simpld ${⊢}{K}\in \mathrm{OP}\to {B}\in \mathrm{dom}\mathrm{lub}\left({K}\right)$
10 9 adantr ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to {B}\in \mathrm{dom}\mathrm{lub}\left({K}\right)$
11 1 4 2 3 5 6 10 ple1