Theorem opoccl 39686

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 2739	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2739	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2739	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2739	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2739	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39674	. . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
9	8	3anidm23 1429	. . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
10	9	simp1d 1148	. 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))))
11	10	simp1d 1148	1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   class class class wbr 5072  ‘cfv 6485  (class class class)co 7356  Basecbs 17170  lecple 17218  occoc 17219  joincjn 18268  meetcmee 18269  0.cp0 18378  1.cp1 18379  OPcops 39664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-nul 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-dm 5628  df-iota 6441  df-fv 6493  df-ov 7359  df-oposet 39668

This theorem is referenced by:  opcon2b  39689  oplecon3b  39692  oplecon1b  39693  opoc1  39694  opltcon3b  39696  opltcon1b  39697  opltcon2b  39698  riotaocN  39701  oldmm1  39709  oldmm2  39710  oldmm3N  39711  oldmm4  39712  oldmj1  39713  oldmj2  39714  oldmj3  39715  oldmj4  39716  olm11  39719  latmassOLD  39721  omllaw2N  39736  omllaw4  39738  cmtcomlemN  39740  cmt2N  39742  cmt3N  39743  cmt4N  39744  cmtbr2N  39745  cmtbr3N  39746  cmtbr4N  39747  lecmtN  39748  omlfh1N  39750  omlfh3N  39751  omlspjN  39753  cvrcon3b  39769  cvrcmp2  39776  atlatmstc  39811  glbconN  39869  glbconxN  39870  cvrexch  39912  1cvrco  39964  1cvratex  39965  1cvrjat  39967  polval2N  40398  polsubN  40399  2polpmapN  40405  2polvalN  40406  poldmj1N  40420  pmapj2N  40421  polatN  40423  2polatN  40424  pnonsingN  40425  ispsubcl2N  40439  polsubclN  40444  poml4N  40445  pmapojoinN  40460  pl42lem1N  40471  lhpoc2N  40507  lhpocnle  40508  lhpmod2i2  40530  lhpmod6i1  40531  lhprelat3N  40532  trlcl  40656  trlle  40676  docaclN  41616  doca2N  41618  djajN  41629  dih1  41778  dih1dimatlem  41821  dochcl  41845  dochvalr3  41855  doch2val2  41856  dochss  41857  dochocss  41858  dochoc  41859  dochnoncon  41883  djhlj  41893