Theorem op0cl

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

	Ref	Expression
Hypotheses	op0cl.b	|- B = ( Base ` K )
	op0cl.z	|- .0. = ( 0. ` K )
Assertion	op0cl	|- ( K e. OP -> .0. e. B )

Proof

Step	Hyp	Ref	Expression
1		op0cl.b	|- B = ( Base ` K )
2		op0cl.z	|- .0. = ( 0. ` K )
3		eqid	|- ( glb ` K ) = ( glb ` K )
4	1 3 2	p0val	|- ( K e. OP -> .0. = ( ( glb ` K ) ` B ) )
5		id	|- ( K e. OP -> K e. OP )
6		eqid	|- ( lub ` K ) = ( lub ` K )
7	1 6 3	op01dm	|- ( K e. OP -> ( B e. dom ( lub ` K ) /\ B e. dom ( glb ` K ) ) )
8	7	simprd	|- ( K e. OP -> B e. dom ( glb ` K ) )
9	1 3 5 8	glbcl	|- ( K e. OP -> ( ( glb ` K ) ` B ) e. B )
10	4 9	eqeltrd	|- ( K e. OP -> .0. e. B )