Theorem op1cl

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

	Ref	Expression
Hypotheses	op1cl.b	|- B = ( Base ` K )
	op1cl.u	|- .1. = ( 1. ` K )
Assertion	op1cl	|- ( K e. OP -> .1. e. B )

Proof

Step	Hyp	Ref	Expression
1		op1cl.b	|- B = ( Base ` K )
2		op1cl.u	|- .1. = ( 1. ` K )
3		eqid	|- ( lub ` K ) = ( lub ` K )
4	1 3 2	p1val	|- ( K e. OP -> .1. = ( ( lub ` K ) ` B ) )
5		id	|- ( K e. OP -> K e. OP )
6		eqid	|- ( glb ` K ) = ( glb ` K )
7	1 3 6	op01dm	|- ( K e. OP -> ( B e. dom ( lub ` K ) /\ B e. dom ( glb ` K ) ) )
8	7	simpld	|- ( K e. OP -> B e. dom ( lub ` K ) )
9	1 3 5 8	lubcl	|- ( K e. OP -> ( ( lub ` K ) ` B ) e. B )
10	4 9	eqeltrd	|- ( K e. OP -> .1. e. B )