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 ⊢BaseK=BaseK
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∧BaseK∈dom⁡lub⁡K∧BaseK∈dom⁡glb⁡K∧∀x∈BaseK∀y∈BaseKoc⁡K⁡x∈BaseK∧oc⁡K⁡oc⁡K⁡x=x∧x≤Ky→oc⁡K⁡y≤Koc⁡K⁡x∧xjoin⁡Koc⁡K⁡x=1.⁡K∧xmeet⁡Koc⁡K⁡x=0.⁡K
11 simpl1 ⊢K∈Poset∧BaseK∈dom⁡lub⁡K∧BaseK∈dom⁡glb⁡K∧∀x∈BaseK∀y∈BaseKoc⁡K⁡x∈BaseK∧oc⁡K⁡oc⁡K⁡x=x∧x≤Ky→oc⁡K⁡y≤Koc⁡K⁡x∧xjoin⁡Koc⁡K⁡x=1.⁡K∧xmeet⁡Koc⁡K⁡x=0.⁡K→K∈Poset
12 10 11 sylbi ⊢K∈OP→K∈Poset