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 𝐵 = ( Base ‘ 𝐾 )
op0le.l = ( le ‘ 𝐾 )
op0le.z 0 = ( 0. ‘ 𝐾 )
Assertion op0le ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 0 𝑋 )

Proof

Step Hyp Ref Expression
1 op0le.b 𝐵 = ( Base ‘ 𝐾 )
2 op0le.l = ( le ‘ 𝐾 )
3 op0le.z 0 = ( 0. ‘ 𝐾 )
4 eqid ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
5 simpl ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 𝐾 ∈ OP )
6 simpr ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 𝑋𝐵 )
7 eqid ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
8 1 7 4 op01dm ( 𝐾 ∈ OP → ( 𝐵 ∈ dom ( lub ‘ 𝐾 ) ∧ 𝐵 ∈ dom ( glb ‘ 𝐾 ) ) )
9 8 simprd ( 𝐾 ∈ OP → 𝐵 ∈ dom ( glb ‘ 𝐾 ) )
10 9 adantr ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 𝐵 ∈ dom ( glb ‘ 𝐾 ) )
11 1 4 2 3 5 6 10 p0le ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → 0 𝑋 )