Theorem ople1

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

	Ref	Expression
Hypotheses	ople1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	ople1.l	⊢ ≤ = ( le ‘ 𝐾 )
	ople1.u	⊢ 1 = ( 1. ‘ 𝐾 )
Assertion	ople1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 1 )

Proof

Step	Hyp	Ref	Expression
1		ople1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		ople1.l	⊢ ≤ = ( le ‘ 𝐾 )
3		ople1.u	⊢ 1 = ( 1. ‘ 𝐾 )
4		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
5		simpl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OP )
6		simpr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
8	1 4 7	op01dm	⊢ ( 𝐾 ∈ OP → ( 𝐵 ∈ dom ( lub ‘ 𝐾 ) ∧ 𝐵 ∈ dom ( glb ‘ 𝐾 ) ) )
9	8	simpld	⊢ ( 𝐾 ∈ OP → 𝐵 ∈ dom ( lub ‘ 𝐾 ) )
10	9	adantr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝐵 ∈ dom ( lub ‘ 𝐾 ) )
11	1 4 2 3 5 6 10	ple1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 1 )