This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )