Theorem opoccl 36345

Description: Closure of orthocomplement operation. (choccl 29083 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

Step	Hyp	Ref	Expression
1		opoccl.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
2		eqid 2821	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2821	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2821	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2821	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2821	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 36333	. . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
9	8	3anidm23 1417	. . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
10	9	simp1d 1138	. 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))))
11	10	simp1d 1138	1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   class class class wbr 5066  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  lecple 16572  occoc 16573  joincjn 17554  meetcmee 17555  0.cp0 17647  1.cp1 17648  OPcops 36323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-dm 5565  df-iota 6314  df-fv 6363  df-ov 7159  df-oposet 36327

This theorem is referenced by:  opcon2b  36348  oplecon3b  36351  oplecon1b  36352  opoc1  36353  opltcon3b  36355  opltcon1b  36356  opltcon2b  36357  riotaocN  36360  oldmm1  36368  oldmm2  36369  oldmm3N  36370  oldmm4  36371  oldmj1  36372  oldmj2  36373  oldmj3  36374  oldmj4  36375  olm11  36378  latmassOLD  36380  omllaw2N  36395  omllaw4  36397  cmtcomlemN  36399  cmt2N  36401  cmt3N  36402  cmt4N  36403  cmtbr2N  36404  cmtbr3N  36405  cmtbr4N  36406  lecmtN  36407  omlfh1N  36409  omlfh3N  36410  omlspjN  36412  cvrcon3b  36428  cvrcmp2  36435  atlatmstc  36470  glbconN  36528  glbconxN  36529  cvrexch  36571  1cvrco  36623  1cvratex  36624  1cvrjat  36626  polval2N  37057  polsubN  37058  2polpmapN  37064  2polvalN  37065  poldmj1N  37079  pmapj2N  37080  polatN  37082  2polatN  37083  pnonsingN  37084  ispsubcl2N  37098  polsubclN  37103  poml4N  37104  pmapojoinN  37119  pl42lem1N  37130  lhpoc2N  37166  lhpocnle  37167  lhpmod2i2  37189  lhpmod6i1  37190  lhprelat3N  37191  trlcl  37315  trlle  37335  docaclN  38275  doca2N  38277  djajN  38288  dih1  38437  dih1dimatlem  38480  dochcl  38504  dochvalr3  38514  doch2val2  38515  dochss  38516  dochocss  38517  dochoc  38518  dochnoncon  38542  djhlj  38552