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 40026
Description: Closure of orthocomplement operation. (choccl 31729 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 2765 . . . . 5 (le‘𝐾) = (le‘𝐾)
3 opoccl.o . . . . 5 = (oc‘𝐾)
4 eqid 2765 . . . . 5 (join‘𝐾) = (join‘𝐾)
5 eqid 2765 . . . . 5 (meet‘𝐾) = (meet‘𝐾)
6 eqid 2765 . . . . 5 (0.‘𝐾) = (0.‘𝐾)
7 eqid 2765 . . . . 5 (1.‘𝐾) = (1.‘𝐾)
81, 2, 3, 4, 5, 6, 7oposlem 40014 . . . 4 ((𝐾 ∈ OP ∧ 𝑋𝐵𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
983anidm23 1448 . . 3 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
109simp1d 1160 . 2 ((𝐾 ∈ OP ∧ 𝑋𝐵) → (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))))
1110simp1d 1160 1 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ( 𝑋) ∈ 𝐵)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wa 401  w3a 1103   = wceq 1570  wcel 2146   class class class wbr 5111  cfv 6540  (class class class)co 7419  Basecbs 17291  lecple 17339  occoc 17340  joincjn 18389  meetcmee 18390  0.cp0 18499  1.cp1 18500  OPcops 40004
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6496  df-fv 6548  df-ov 7422  df-oposet 40008
This theorem is used by:  opcon2b  40029  oplecon3b  40032  oplecon1b  40033  opoc1  40034  opltcon3b  40036  opltcon1b  40037  opltcon2b  40038  riotaocN  40041  oldmm1  40049  oldmm2  40050  oldmm3N  40051  oldmm4  40052  oldmj1  40053  oldmj2  40054  oldmj3  40055  oldmj4  40056  olm11  40059  latmassOLD  40061  omllaw2N  40076  omllaw4  40078  cmtcomlemN  40080  cmt2N  40082  cmt3N  40083  cmt4N  40084  cmtbr2N  40085  cmtbr3N  40086  cmtbr4N  40087  lecmtN  40088  omlfh1N  40090  omlfh3N  40091  omlspjN  40093  cvrcon3b  40109  cvrcmp2  40116  atlatmstc  40151  glbconN  40209  glbconxN  40210  cvrexch  40252  1cvrco  40304  1cvratex  40305  1cvrjat  40307  polval2N  40738  polsubN  40739  2polpmapN  40745  2polvalN  40746  poldmj1N  40760  pmapj2N  40761  polatN  40763  2polatN  40764  pnonsingN  40765  ispsubcl2N  40779  polsubclN  40784  poml4N  40785  pmapojoinN  40800  pl42lem1N  40811  lhpoc2N  40847  lhpocnle  40848  lhpmod2i2  40870  lhpmod6i1  40871  lhprelat3N  40872  trlcl  40996  trlle  41016  docaclN  41956  doca2N  41958  djajN  41969  dih1  42118  dih1dimatlem  42161  dochcl  42185  dochvalr3  42195  doch2val2  42196  dochss  42197  dochocss  42198  dochoc  42199  dochnoncon  42223  djhlj  42233
  Copyright terms: Public domain W3C validator