This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem op0cl

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

Ref Expression
Hypotheses op0cl.b ⊢ B = Base K
op0cl.z ⊢ 0 ˙ = 0. ⁡ K
Assertion op0cl ⊢ K ∈ OP → 0 ˙ ∈ B

Proof

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