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
|- .<_ = ( le ` K )
op0le.z
|- .0. = ( 0. ` K )
Assertion op0le
|- ( ( K e. OP /\ X e. B ) -> .0. .<_ X )

Proof

Step Hyp Ref Expression
1 op0le.b
 |-  B = ( Base ` K )
2 op0le.l
 |-  .<_ = ( le ` K )
3 op0le.z
 |-  .0. = ( 0. ` K )
4 eqid
 |-  ( glb ` K ) = ( glb ` K )
5 simpl
 |-  ( ( K e. OP /\ X e. B ) -> K e. OP )
6 simpr
 |-  ( ( K e. OP /\ X e. B ) -> X e. B )
7 eqid
 |-  ( lub ` K ) = ( lub ` K )
8 1 7 4 op01dm
 |-  ( K e. OP -> ( B e. dom ( lub ` K ) /\ B e. dom ( glb ` K ) ) )
9 8 simprd
 |-  ( K e. OP -> B e. dom ( glb ` K ) )
10 9 adantr
 |-  ( ( K e. OP /\ X e. B ) -> B e. dom ( glb ` K ) )
11 1 4 2 3 5 6 10 p0le
 |-  ( ( K e. OP /\ X e. B ) -> .0. .<_ X )