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

Metamath Proof Explorer

Theorem ople1

Description: Any element is less than the orthoposet unity. ( chss analog.) (Contributed by NM, 23-Oct-2011)

Ref Expression
Hypotheses ople1.b 
|- B = ( Base ` K )
ople1.l 
|- .<_ = ( le ` K )
ople1.u 
|- .1. = ( 1. ` K )
Assertion ople1 
|- ( ( K e. OP /\ X e. B ) -> X .<_ .1. )

Proof

Step Hyp Ref Expression
1 ople1.b 
 |-  B = ( Base ` K )
2 ople1.l 
 |-  .<_ = ( le ` K )
3 ople1.u 
 |-  .1. = ( 1. ` K )
4 eqid 
 |-  ( lub ` K ) = ( lub ` 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 
 |-  ( glb ` K ) = ( glb ` K )
8 1 4 7 op01dm 
 |-  ( K e. OP -> ( B e. dom ( lub ` K ) /\ B e. dom ( glb ` K ) ) )
9 8 simpld 
 |-  ( K e. OP -> B e. dom ( lub ` K ) )
10 9 adantr 
 |-  ( ( K e. OP /\ X e. B ) -> B e. dom ( lub ` K ) )
11 1 4 2 3 5 6 10 ple1 
 |-  ( ( K e. OP /\ X e. B ) -> X .<_ .1. )