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 𝐵 = ( Base ‘ 𝐾 )
op1cl.u 1 = ( 1. ‘ 𝐾 )
Assertion op1cl ( 𝐾 ∈ OP → 1𝐵 )

Proof

Step Hyp Ref Expression
1 op1cl.b 𝐵 = ( Base ‘ 𝐾 )
2 op1cl.u 1 = ( 1. ‘ 𝐾 )
3 eqid ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
4 1 3 2 p1val ( 𝐾 ∈ OP → 1 = ( ( lub ‘ 𝐾 ) ‘ 𝐵 ) )
5 id ( 𝐾 ∈ OP → 𝐾 ∈ OP )
6 eqid ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
7 1 3 6 op01dm ( 𝐾 ∈ OP → ( 𝐵 ∈ dom ( lub ‘ 𝐾 ) ∧ 𝐵 ∈ dom ( glb ‘ 𝐾 ) ) )
8 7 simpld ( 𝐾 ∈ OP → 𝐵 ∈ dom ( lub ‘ 𝐾 ) )
9 1 3 5 8 lubcl ( 𝐾 ∈ OP → ( ( lub ‘ 𝐾 ) ‘ 𝐵 ) ∈ 𝐵 )
10 4 9 eqeltrd ( 𝐾 ∈ OP → 1𝐵 )