Theorem op0cl

Description: An orthoposet has a zero element. ( h0elch analog.) (Contributed by NM, 12-Oct-2011)

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

Proof

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