Theorem op1cl

Description: An orthoposet has a unity element. ( helch analog.) (Contributed by NM, 22-Oct-2011)

	Ref	Expression
Hypotheses	op1cl.b	$$⊢B={\mathrm{Base}}_K$$
	op1cl.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	op1cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in B$$

Proof

Step	Hyp	Ref	Expression
1		op1cl.b	$$⊢B={\mathrm{Base}}_K$$
2		op1cl.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
3		eqid	$$⊢\mathrm{lub}\left(K\right)=\mathrm{lub}\left(K\right)$$
4	1 3 2	p1val	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}=\mathrm{lub}\left(K\right)\left(B\right)$$
5		id	$$⊢K\in \mathrm{OP}\to K\in \mathrm{OP}$$
6		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
7	1 3 6	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)$$
8	7	simpld	$$⊢K\in \mathrm{OP}\to B\in \mathrm{dom}\mathrm{lub}\left(K\right)$$
9	1 3 5 8	lubcl	$$⊢K\in \mathrm{OP}\to \mathrm{lub}\left(K\right)\left(B\right)\in B$$
10	4 9	eqeltrd	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in B$$