Theorem opoccl 33499

Description: Closure of orthocomplement operation. (choccl 27549 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 2610	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2610	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2610	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2610	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2610	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 33487	. . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
9	8	3anidm23 1377	. . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
10	9	simp1d 1066	. 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))))
11	10	simp1d 1066	1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  lecple 15775  occoc 15776  joincjn 16767  meetcmee 16768  0.cp0 16860  1.cp1 16861  OPcops 33477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-dm 5048  df-iota 5768  df-fv 5812  df-ov 6552  df-oposet 33481

This theorem is referenced by:  opcon2b  33502  oplecon3b  33505  oplecon1b  33506  opoc1  33507  opltcon3b  33509  opltcon1b  33510  opltcon2b  33511  riotaocN  33514  oldmm1  33522  oldmm2  33523  oldmm3N  33524  oldmm4  33525  oldmj1  33526  oldmj2  33527  oldmj3  33528  oldmj4  33529  olm11  33532  latmassOLD  33534  omllaw2N  33549  omllaw4  33551  cmtcomlemN  33553  cmt2N  33555  cmt3N  33556  cmt4N  33557  cmtbr2N  33558  cmtbr3N  33559  cmtbr4N  33560  lecmtN  33561  omlfh1N  33563  omlfh3N  33564  omlspjN  33566  cvrcon3b  33582  cvrcmp2  33589  atlatmstc  33624  glbconN  33681  glbconxN  33682  cvrexch  33724  1cvrco  33776  1cvratex  33777  1cvrjat  33779  polval2N  34210  polsubN  34211  2polpmapN  34217  2polvalN  34218  poldmj1N  34232  pmapj2N  34233  polatN  34235  2polatN  34236  pnonsingN  34237  ispsubcl2N  34251  polsubclN  34256  poml4N  34257  pmapojoinN  34272  pl42lem1N  34283  lhpoc2N  34319  lhpocnle  34320  lhpmod2i2  34342  lhpmod6i1  34343  lhprelat3N  34344  trlcl  34469  trlle  34489  docaclN  35431  doca2N  35433  djajN  35444  dih1  35593  dih1dimatlem  35636  dochcl  35660  dochvalr3  35670  doch2val2  35671  dochss  35672  dochocss  35673  dochoc  35674  dochnoncon  35698  djhlj  35708