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

Theorem opoccl 36509
 Description: Closure of orthocomplement operation. (choccl 29099 analog.) (Contributed by NM, 20-Oct-2011.)
Hypotheses
Ref Expression
opoccl.b 𝐵 = (Base‘𝐾)
opoccl.o = (oc‘𝐾)
Assertion
Ref Expression
opoccl ((𝐾 ∈ OP ∧ 𝑋𝐵) → ( 𝑋) ∈ 𝐵)

Proof of Theorem opoccl
StepHypRef Expression
1 opoccl.b . . . . 5 𝐵 = (Base‘𝐾)
2 eqid 2798 . . . . 5 (le‘𝐾) = (le‘𝐾)
3 opoccl.o . . . . 5 = (oc‘𝐾)
4 eqid 2798 . . . . 5 (join‘𝐾) = (join‘𝐾)
5 eqid 2798 . . . . 5 (meet‘𝐾) = (meet‘𝐾)
6 eqid 2798 . . . . 5 (0.‘𝐾) = (0.‘𝐾)
7 eqid 2798 . . . . 5 (1.‘𝐾) = (1.‘𝐾)
81, 2, 3, 4, 5, 6, 7oposlem 36497 . . . 4 ((𝐾 ∈ OP ∧ 𝑋𝐵𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
983anidm23 1418 . . 3 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
109simp1d 1139 . 2 ((𝐾 ∈ OP ∧ 𝑋𝐵) → (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))))
1110simp1d 1139 1 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ( 𝑋) ∈ 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   class class class wbr 5031  ‘cfv 6325  (class class class)co 7136  Basecbs 16478  lecple 16567  occoc 16568  joincjn 17549  meetcmee 17550  0.cp0 17642  1.cp1 17643  OPcops 36487 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5175 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5032  df-dm 5530  df-iota 6284  df-fv 6333  df-ov 7139  df-oposet 36491 This theorem is referenced by:  opcon2b  36512  oplecon3b  36515  oplecon1b  36516  opoc1  36517  opltcon3b  36519  opltcon1b  36520  opltcon2b  36521  riotaocN  36524  oldmm1  36532  oldmm2  36533  oldmm3N  36534  oldmm4  36535  oldmj1  36536  oldmj2  36537  oldmj3  36538  oldmj4  36539  olm11  36542  latmassOLD  36544  omllaw2N  36559  omllaw4  36561  cmtcomlemN  36563  cmt2N  36565  cmt3N  36566  cmt4N  36567  cmtbr2N  36568  cmtbr3N  36569  cmtbr4N  36570  lecmtN  36571  omlfh1N  36573  omlfh3N  36574  omlspjN  36576  cvrcon3b  36592  cvrcmp2  36599  atlatmstc  36634  glbconN  36692  glbconxN  36693  cvrexch  36735  1cvrco  36787  1cvratex  36788  1cvrjat  36790  polval2N  37221  polsubN  37222  2polpmapN  37228  2polvalN  37229  poldmj1N  37243  pmapj2N  37244  polatN  37246  2polatN  37247  pnonsingN  37248  ispsubcl2N  37262  polsubclN  37267  poml4N  37268  pmapojoinN  37283  pl42lem1N  37294  lhpoc2N  37330  lhpocnle  37331  lhpmod2i2  37353  lhpmod6i1  37354  lhprelat3N  37355  trlcl  37479  trlle  37499  docaclN  38439  doca2N  38441  djajN  38452  dih1  38601  dih1dimatlem  38644  dochcl  38668  dochvalr3  38678  doch2val2  38679  dochss  38680  dochocss  38681  dochoc  38682  dochnoncon  38706  djhlj  38716
 Copyright terms: Public domain W3C validator