Theorem op0cl

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

	Ref	Expression
Hypotheses	op0cl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	op0cl.z	⊢ 0 = ( 0. ‘ 𝐾 )
Assertion	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		op0cl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		op0cl.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
4	1 3 2	p0val	⊢ ( 𝐾 ∈ OP → 0 = ( ( glb ‘ 𝐾 ) ‘ 𝐵 ) )
5		id	⊢ ( 𝐾 ∈ OP → 𝐾 ∈ OP )
6		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
7	1 6 3	op01dm	⊢ ( 𝐾 ∈ OP → ( 𝐵 ∈ dom ( lub ‘ 𝐾 ) ∧ 𝐵 ∈ dom ( glb ‘ 𝐾 ) ) )
8	7	simprd	⊢ ( 𝐾 ∈ OP → 𝐵 ∈ dom ( glb ‘ 𝐾 ) )
9	1 3 5 8	glbcl	⊢ ( 𝐾 ∈ OP → ( ( glb ‘ 𝐾 ) ‘ 𝐵 ) ∈ 𝐵 )
10	4 9	eqeltrd	⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 )