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

Theorem opoccl 34901
Description: Closure of orthocomplement operation. (choccl 28395 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 2724 . . . . 5 (le‘𝐾) = (le‘𝐾)
3 opoccl.o . . . . 5 = (oc‘𝐾)
4 eqid 2724 . . . . 5 (join‘𝐾) = (join‘𝐾)
5 eqid 2724 . . . . 5 (meet‘𝐾) = (meet‘𝐾)
6 eqid 2724 . . . . 5 (0.‘𝐾) = (0.‘𝐾)
7 eqid 2724 . . . . 5 (1.‘𝐾) = (1.‘𝐾)
81, 2, 3, 4, 5, 6, 7oposlem 34889 . . . 4 ((𝐾 ∈ OP ∧ 𝑋𝐵𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
983anidm23 1498 . . 3 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
109simp1d 1134 . 2 ((𝐾 ∈ OP ∧ 𝑋𝐵) → (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))))
1110simp1d 1134 1 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ( 𝑋) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1596  wcel 2103   class class class wbr 4760  cfv 6001  (class class class)co 6765  Basecbs 15980  lecple 16071  occoc 16072  joincjn 17066  meetcmee 17067  0.cp0 17159  1.cp1 17160  OPcops 34879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-nul 4897
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-dm 5228  df-iota 5964  df-fv 6009  df-ov 6768  df-oposet 34883
This theorem is referenced by:  opcon2b  34904  oplecon3b  34907  oplecon1b  34908  opoc1  34909  opltcon3b  34911  opltcon1b  34912  opltcon2b  34913  riotaocN  34916  oldmm1  34924  oldmm2  34925  oldmm3N  34926  oldmm4  34927  oldmj1  34928  oldmj2  34929  oldmj3  34930  oldmj4  34931  olm11  34934  latmassOLD  34936  omllaw2N  34951  omllaw4  34953  cmtcomlemN  34955  cmt2N  34957  cmt3N  34958  cmt4N  34959  cmtbr2N  34960  cmtbr3N  34961  cmtbr4N  34962  lecmtN  34963  omlfh1N  34965  omlfh3N  34966  omlspjN  34968  cvrcon3b  34984  cvrcmp2  34991  atlatmstc  35026  glbconN  35083  glbconxN  35084  cvrexch  35126  1cvrco  35178  1cvratex  35179  1cvrjat  35181  polval2N  35612  polsubN  35613  2polpmapN  35619  2polvalN  35620  poldmj1N  35634  pmapj2N  35635  polatN  35637  2polatN  35638  pnonsingN  35639  ispsubcl2N  35653  polsubclN  35658  poml4N  35659  pmapojoinN  35674  pl42lem1N  35685  lhpoc2N  35721  lhpocnle  35722  lhpmod2i2  35744  lhpmod6i1  35745  lhprelat3N  35746  trlcl  35871  trlle  35891  docaclN  36832  doca2N  36834  djajN  36845  dih1  36994  dih1dimatlem  37037  dochcl  37061  dochvalr3  37071  doch2val2  37072  dochss  37073  dochocss  37074  dochoc  37075  dochnoncon  37099  djhlj  37109
  Copyright terms: Public domain W3C validator