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

Metamath Proof Explorer

Theorem op1cl

Description: An orthoposet has a unity 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 ∈ OP → 1 ˙ ∈ 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 ∈ OP → 1 ˙ = lub ⁡ K ⁡ B
5 id ⊢ K ∈ OP → K ∈ OP
6 eqid ⊢ glb ⁡ K = glb ⁡ K
7 1 3 6 op01dm ⊢ K ∈ OP → B ∈ dom ⁡ lub ⁡ K ∧ B ∈ dom ⁡ glb ⁡ K
8 7 simpld ⊢ K ∈ OP → B ∈ dom ⁡ lub ⁡ K
9 1 3 5 8 lubcl ⊢ K ∈ OP → lub ⁡ K ⁡ B ∈ B
10 4 9 eqeltrd ⊢ K ∈ OP → 1 ˙ ∈ B