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 ≤ 𝑋 )