Theorem opposet 39753

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

Assertion

Ref	Expression
opposet	⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset)

Proof of Theorem opposet

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2756	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		eqid 2756	. . 3 ⊢ (lub‘𝐾) = (lub‘𝐾)
3		eqid 2756	. . 3 ⊢ (glb‘𝐾) = (glb‘𝐾)
4		eqid 2756	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
5		eqid 2756	. . 3 ⊢ (oc‘𝐾) = (oc‘𝐾)
6		eqid 2756	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
7		eqid 2756	. . 3 ⊢ (meet‘𝐾) = (meet‘𝐾)
8		eqid 2756	. . 3 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2756	. . 3 ⊢ (1.‘𝐾) = (1.‘𝐾)
10	1, 2, 3, 4, 5, 6, 7, 8, 9	isopos 39752	. 2 ⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ (Base‘𝐾) ∈ dom (lub‘𝐾) ∧ (Base‘𝐾) ∈ dom (glb‘𝐾)) ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)((((oc‘𝐾)‘𝑥) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))))
11		simpl1 1201	. 2 ⊢ (((𝐾 ∈ Poset ∧ (Base‘𝐾) ∈ dom (lub‘𝐾) ∧ (Base‘𝐾) ∈ dom (glb‘𝐾)) ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)((((oc‘𝐾)‘𝑥) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))) → 𝐾 ∈ Poset)
12	10, 11	sylbi 219	1 ⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095   = wceq 1554   ∈ wcel 2136  ∀wral 3070   class class class wbr 5094  dom cdm 5640  ‘cfv 6510  (class class class)co 7385  Basecbs 17221  lecple 17269  occoc 17270  Posetcpo 18315  lubclub 18317  glbcglb 18318  joincjn 18319  meetcmee 18320  0.cp0 18429  1.cp1 18430  OPcops 39744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-nul 5250

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-dm 5650  df-iota 6466  df-fv 6518  df-ov 7388  df-oposet 39748

This theorem is referenced by:  ople0  39759  op1le  39764  opltcon3b  39776  olposN  39787  ncvr1  39844  cvrcmp2  39856  leatb  39864  dalemcea  40232