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

Theorem op0le 36973
Description: Orthoposet zero is less than or equal to any element. (ch0le 29553 analog.) (Contributed by NM, 12-Oct-2011.)
Hypotheses
Ref Expression
op0le.b 𝐵 = (Base‘𝐾)
op0le.l = (le‘𝐾)
op0le.z 0 = (0.‘𝐾)
Assertion
Ref Expression
op0le ((𝐾 ∈ OP ∧ 𝑋𝐵) → 0 𝑋)

Proof of Theorem op0le
StepHypRef Expression
1 op0le.b . 2 𝐵 = (Base‘𝐾)
2 eqid 2739 . 2 (glb‘𝐾) = (glb‘𝐾)
3 op0le.l . 2 = (le‘𝐾)
4 op0le.z . 2 0 = (0.‘𝐾)
5 simpl 486 . 2 ((𝐾 ∈ OP ∧ 𝑋𝐵) → 𝐾 ∈ OP)
6 simpr 488 . 2 ((𝐾 ∈ OP ∧ 𝑋𝐵) → 𝑋𝐵)
7 eqid 2739 . . . . 5 (lub‘𝐾) = (lub‘𝐾)
81, 7, 2op01dm 36970 . . . 4 (𝐾 ∈ OP → (𝐵 ∈ dom (lub‘𝐾) ∧ 𝐵 ∈ dom (glb‘𝐾)))
98simprd 499 . . 3 (𝐾 ∈ OP → 𝐵 ∈ dom (glb‘𝐾))
109adantr 484 . 2 ((𝐾 ∈ OP ∧ 𝑋𝐵) → 𝐵 ∈ dom (glb‘𝐾))
111, 2, 3, 4, 5, 6, 10p0le 17967 1 ((𝐾 ∈ OP ∧ 𝑋𝐵) → 0 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2112   class class class wbr 5069  dom cdm 5568  cfv 6400  Basecbs 16792  lecple 16841  lubclub 17848  glbcglb 17849  0.cp0 17961  OPcops 36959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-id 5471  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-glb 17885  df-p0 17963  df-oposet 36963
This theorem is referenced by:  ople0  36974  opnlen0  36975  lub0N  36976  opltn0  36977  olj01  37012  olm01  37023  leatb  37079  1cvratex  37260  llnn0  37303  lplnn0N  37334  lvoln0N  37378  dalemcea  37447  ltrnatb  37924  tendo0tp  38576  cdlemk39s-id  38727  dia0eldmN  38827  dib0  38951  dih0  39067  dihmeetlem18N  39111
  Copyright terms: Public domain W3C validator