Metamath Proof Explorer


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 )