Theorem opoccl 39657

Description: Closure of orthocomplement operation. (choccl 31395 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 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.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39645	. . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
9	8	3anidm23 1424	. . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
10	9	simp1d 1143	. 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))))
11	10	simp1d 1143	1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6493  (class class class)co 7361  Basecbs 17173  lecple 17221  occoc 17222  joincjn 18271  meetcmee 18272  0.cp0 18381  1.cp1 18382  OPcops 39635

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-dm 5635  df-iota 6449  df-fv 6501  df-ov 7364  df-oposet 39639

This theorem is referenced by:  opcon2b  39660  oplecon3b  39663  oplecon1b  39664  opoc1  39665  opltcon3b  39667  opltcon1b  39668  opltcon2b  39669  riotaocN  39672  oldmm1  39680  oldmm2  39681  oldmm3N  39682  oldmm4  39683  oldmj1  39684  oldmj2  39685  oldmj3  39686  oldmj4  39687  olm11  39690  latmassOLD  39692  omllaw2N  39707  omllaw4  39709  cmtcomlemN  39711  cmt2N  39713  cmt3N  39714  cmt4N  39715  cmtbr2N  39716  cmtbr3N  39717  cmtbr4N  39718  lecmtN  39719  omlfh1N  39721  omlfh3N  39722  omlspjN  39724  cvrcon3b  39740  cvrcmp2  39747  atlatmstc  39782  glbconN  39840  glbconxN  39841  cvrexch  39883  1cvrco  39935  1cvratex  39936  1cvrjat  39938  polval2N  40369  polsubN  40370  2polpmapN  40376  2polvalN  40377  poldmj1N  40391  pmapj2N  40392  polatN  40394  2polatN  40395  pnonsingN  40396  ispsubcl2N  40410  polsubclN  40415  poml4N  40416  pmapojoinN  40431  pl42lem1N  40442  lhpoc2N  40478  lhpocnle  40479  lhpmod2i2  40501  lhpmod6i1  40502  lhprelat3N  40503  trlcl  40627  trlle  40647  docaclN  41587  doca2N  41589  djajN  41600  dih1  41749  dih1dimatlem  41792  dochcl  41816  dochvalr3  41826  doch2val2  41827  dochss  41828  dochocss  41829  dochoc  41830  dochnoncon  41854  djhlj  41864