Theorem opoccl 39393

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   class class class wbr 5096  ‘cfv 6490  (class class class)co 7356  Basecbs 17134  lecple 17182  occoc 17183  joincjn 18232  meetcmee 18233  0.cp0 18342  1.cp1 18343  OPcops 39371

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-nul 5249

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-dm 5632  df-iota 6446  df-fv 6498  df-ov 7359  df-oposet 39375

This theorem is referenced by:  opcon2b  39396  oplecon3b  39399  oplecon1b  39400  opoc1  39401  opltcon3b  39403  opltcon1b  39404  opltcon2b  39405  riotaocN  39408  oldmm1  39416  oldmm2  39417  oldmm3N  39418  oldmm4  39419  oldmj1  39420  oldmj2  39421  oldmj3  39422  oldmj4  39423  olm11  39426  latmassOLD  39428  omllaw2N  39443  omllaw4  39445  cmtcomlemN  39447  cmt2N  39449  cmt3N  39450  cmt4N  39451  cmtbr2N  39452  cmtbr3N  39453  cmtbr4N  39454  lecmtN  39455  omlfh1N  39457  omlfh3N  39458  omlspjN  39460  cvrcon3b  39476  cvrcmp2  39483  atlatmstc  39518  glbconN  39576  glbconxN  39577  cvrexch  39619  1cvrco  39671  1cvratex  39672  1cvrjat  39674  polval2N  40105  polsubN  40106  2polpmapN  40112  2polvalN  40113  poldmj1N  40127  pmapj2N  40128  polatN  40130  2polatN  40131  pnonsingN  40132  ispsubcl2N  40146  polsubclN  40151  poml4N  40152  pmapojoinN  40167  pl42lem1N  40178  lhpoc2N  40214  lhpocnle  40215  lhpmod2i2  40237  lhpmod6i1  40238  lhprelat3N  40239  trlcl  40363  trlle  40383  docaclN  41323  doca2N  41325  djajN  41336  dih1  41485  dih1dimatlem  41528  dochcl  41552  dochvalr3  41562  doch2val2  41563  dochss  41564  dochocss  41565  dochoc  41566  dochnoncon  41590  djhlj  41600