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 37659
Description: Closure of orthocomplement operation. (choccl 30251 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 2737 . . . . 5 (leβ€˜πΎ) = (leβ€˜πΎ)
3 opoccl.o . . . . 5 βŠ₯ = (ocβ€˜πΎ)
4 eqid 2737 . . . . 5 (joinβ€˜πΎ) = (joinβ€˜πΎ)
5 eqid 2737 . . . . 5 (meetβ€˜πΎ) = (meetβ€˜πΎ)
6 eqid 2737 . . . . 5 (0.β€˜πΎ) = (0.β€˜πΎ)
7 eqid 2737 . . . . 5 (1.β€˜πΎ) = (1.β€˜πΎ)
81, 2, 3, 4, 5, 6, 7oposlem 37647 . . . 4 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋(leβ€˜πΎ)𝑋 β†’ ( βŠ₯ β€˜π‘‹)(leβ€˜πΎ)( βŠ₯ β€˜π‘‹))) ∧ (𝑋(joinβ€˜πΎ)( βŠ₯ β€˜π‘‹)) = (1.β€˜πΎ) ∧ (𝑋(meetβ€˜πΎ)( βŠ₯ β€˜π‘‹)) = (0.β€˜πΎ)))
983anidm23 1422 . . 3 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋(leβ€˜πΎ)𝑋 β†’ ( βŠ₯ β€˜π‘‹)(leβ€˜πΎ)( βŠ₯ β€˜π‘‹))) ∧ (𝑋(joinβ€˜πΎ)( βŠ₯ β€˜π‘‹)) = (1.β€˜πΎ) ∧ (𝑋(meetβ€˜πΎ)( βŠ₯ β€˜π‘‹)) = (0.β€˜πΎ)))
109simp1d 1143 . 2 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ (( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋(leβ€˜πΎ)𝑋 β†’ ( βŠ₯ β€˜π‘‹)(leβ€˜πΎ)( βŠ₯ β€˜π‘‹))))
1110simp1d 1143 1 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘‹) ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   class class class wbr 5106  β€˜cfv 6497  (class class class)co 7358  Basecbs 17084  lecple 17141  occoc 17142  joincjn 18201  meetcmee 18202  0.cp0 18313  1.cp1 18314  OPcops 37637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-nul 5264
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-dm 5644  df-iota 6449  df-fv 6505  df-ov 7361  df-oposet 37641
This theorem is referenced by:  opcon2b  37662  oplecon3b  37665  oplecon1b  37666  opoc1  37667  opltcon3b  37669  opltcon1b  37670  opltcon2b  37671  riotaocN  37674  oldmm1  37682  oldmm2  37683  oldmm3N  37684  oldmm4  37685  oldmj1  37686  oldmj2  37687  oldmj3  37688  oldmj4  37689  olm11  37692  latmassOLD  37694  omllaw2N  37709  omllaw4  37711  cmtcomlemN  37713  cmt2N  37715  cmt3N  37716  cmt4N  37717  cmtbr2N  37718  cmtbr3N  37719  cmtbr4N  37720  lecmtN  37721  omlfh1N  37723  omlfh3N  37724  omlspjN  37726  cvrcon3b  37742  cvrcmp2  37749  atlatmstc  37784  glbconN  37842  glbconNOLD  37843  glbconxN  37844  cvrexch  37886  1cvrco  37938  1cvratex  37939  1cvrjat  37941  polval2N  38372  polsubN  38373  2polpmapN  38379  2polvalN  38380  poldmj1N  38394  pmapj2N  38395  polatN  38397  2polatN  38398  pnonsingN  38399  ispsubcl2N  38413  polsubclN  38418  poml4N  38419  pmapojoinN  38434  pl42lem1N  38445  lhpoc2N  38481  lhpocnle  38482  lhpmod2i2  38504  lhpmod6i1  38505  lhprelat3N  38506  trlcl  38630  trlle  38650  docaclN  39590  doca2N  39592  djajN  39603  dih1  39752  dih1dimatlem  39795  dochcl  39819  dochvalr3  39829  doch2val2  39830  dochss  39831  dochocss  39832  dochoc  39833  dochnoncon  39857  djhlj  39867
  Copyright terms: Public domain W3C validator