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={\mathrm{Base}}_K$$
	ople1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ople1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	ople1	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X\underset{\dot{}}{\le }\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		ople1.b	$$⊢B={\mathrm{Base}}_K$$
2		ople1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		ople1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
4		eqid	$$⊢\mathrm{lub}\left(K\right)=\mathrm{lub}\left(K\right)$$
5		simpl	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to K\in \mathrm{OP}$$
6		simpr	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X\in B$$
7		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
8	1 4 7	op01dm	$$⊢K\in \mathrm{OP}\to \left(B\in \mathrm{dom}\mathrm{lub}\left(K\right)\wedge B\in \mathrm{dom}\mathrm{glb}\left(K\right)\right)$$
9	8	simpld	$$⊢K\in \mathrm{OP}\to B\in \mathrm{dom}\mathrm{lub}\left(K\right)$$
10	9	adantr	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to B\in \mathrm{dom}\mathrm{lub}\left(K\right)$$
11	1 4 2 3 5 6 10	ple1	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X\underset{\dot{}}{\le }\underset{\dot{}}{1}$$