Theorem op1cl

Description: An orthoposet has a unity 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 ∈ 𝐵 )