Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  op01dm Structured version   Visualization version   GIF version

Theorem op01dm 39184
Description: Conditions necessary for zero and unity elements to exist. (Contributed by NM, 14-Sep-2018.)
Hypotheses
Ref Expression
op01dm.b 𝐵 = (Base‘𝐾)
op01dm.u 𝑈 = (lub‘𝐾)
op01dm.g 𝐺 = (glb‘𝐾)
Assertion
Ref Expression
op01dm (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺))

Proof of Theorem op01dm
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 op01dm.b . . 3 𝐵 = (Base‘𝐾)
2 op01dm.u . . 3 𝑈 = (lub‘𝐾)
3 op01dm.g . . 3 𝐺 = (glb‘𝐾)
4 eqid 2737 . . 3 (le‘𝐾) = (le‘𝐾)
5 eqid 2737 . . 3 (oc‘𝐾) = (oc‘𝐾)
6 eqid 2737 . . 3 (join‘𝐾) = (join‘𝐾)
7 eqid 2737 . . 3 (meet‘𝐾) = (meet‘𝐾)
8 eqid 2737 . . 3 (0.‘𝐾) = (0.‘𝐾)
9 eqid 2737 . . 3 (1.‘𝐾) = (1.‘𝐾)
101, 2, 3, 4, 5, 6, 7, 8, 9isopos 39181 . 2 (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∀𝑥𝐵𝑦𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))))
11 simpl 482 . . 3 (((𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∀𝑥𝐵𝑦𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))) → (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺))
12113adantl1 1167 . 2 (((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺) ∧ ∀𝑥𝐵𝑦𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))) → (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺))
1310, 12sylbi 217 1 (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈𝐵 ∈ dom 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061   class class class wbr 5143  dom cdm 5685  cfv 6561  (class class class)co 7431  Basecbs 17247  lecple 17304  occoc 17305  Posetcpo 18353  lubclub 18355  glbcglb 18356  joincjn 18357  meetcmee 18358  0.cp0 18468  1.cp1 18469  OPcops 39173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-dm 5695  df-iota 6514  df-fv 6569  df-ov 7434  df-oposet 39177
This theorem is referenced by:  op0cl  39185  op1cl  39186  op0le  39187  ople1  39192  lhp2lt  40003
  Copyright terms: Public domain W3C validator