Metamath Proof Explorer

Theorem opposet

Description: Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011)

Ref Expression
Assertion opposet ⊢ K ∈ OP → K ∈ Poset

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base K = Base K
2 eqid ⊢ lub ⁡ K = lub ⁡ K
3 eqid ⊢ glb ⁡ K = glb ⁡ K
4 eqid ⊢ ≤ K = ≤ K
5 eqid ⊢ oc ⁡ K = oc ⁡ K
6 eqid ⊢ join ⁡ K = join ⁡ K
7 eqid ⊢ meet ⁡ K = meet ⁡ K
8 eqid ⊢ 0. ⁡ K = 0. ⁡ K
9 eqid ⊢ 1. ⁡ K = 1. ⁡ K
10 1 2 3 4 5 6 7 8 9 isopos ⊢ K ∈ OP ↔ K ∈ Poset ∧ Base K ∈ dom ⁡ lub ⁡ K ∧ Base K ∈ dom ⁡ glb ⁡ K ∧ ∀ x ∈ Base K ∀ y ∈ Base K oc ⁡ K ⁡ x ∈ Base K ∧ oc ⁡ K ⁡ oc ⁡ K ⁡ x = x ∧ x ≤ K y → oc ⁡ K ⁡ y ≤ K oc ⁡ K ⁡ x ∧ x join ⁡ K oc ⁡ K ⁡ x = 1. ⁡ K ∧ x meet ⁡ K oc ⁡ K ⁡ x = 0. ⁡ K
11 simpl1 ⊢ K ∈ Poset ∧ Base K ∈ dom ⁡ lub ⁡ K ∧ Base K ∈ dom ⁡ glb ⁡ K ∧ ∀ x ∈ Base K ∀ y ∈ Base K oc ⁡ K ⁡ x ∈ Base K ∧ oc ⁡ K ⁡ oc ⁡ K ⁡ x = x ∧ x ≤ K y → oc ⁡ K ⁡ y ≤ K oc ⁡ K ⁡ x ∧ x join ⁡ K oc ⁡ K ⁡ x = 1. ⁡ K ∧ x meet ⁡ K oc ⁡ K ⁡ x = 0. ⁡ K → K ∈ Poset
12 10 11 sylbi ⊢ K ∈ OP → K ∈ Poset