Theorem opoccl 38053

Description: Closure of orthocomplement operation. (choccl 30547 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 2733	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2733	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2733	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2733	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2733	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 38041	. . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
9	8	3anidm23 1422	. . 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 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   class class class wbr 5148  ‘cfv 6541  (class class class)co 7406  Basecbs 17141  lecple 17201  occoc 17202  joincjn 18261  meetcmee 18262  0.cp0 18373  1.cp1 18374  OPcops 38031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-dm 5686  df-iota 6493  df-fv 6549  df-ov 7409  df-oposet 38035

This theorem is referenced by:  opcon2b  38056  oplecon3b  38059  oplecon1b  38060  opoc1  38061  opltcon3b  38063  opltcon1b  38064  opltcon2b  38065  riotaocN  38068  oldmm1  38076  oldmm2  38077  oldmm3N  38078  oldmm4  38079  oldmj1  38080  oldmj2  38081  oldmj3  38082  oldmj4  38083  olm11  38086  latmassOLD  38088  omllaw2N  38103  omllaw4  38105  cmtcomlemN  38107  cmt2N  38109  cmt3N  38110  cmt4N  38111  cmtbr2N  38112  cmtbr3N  38113  cmtbr4N  38114  lecmtN  38115  omlfh1N  38117  omlfh3N  38118  omlspjN  38120  cvrcon3b  38136  cvrcmp2  38143  atlatmstc  38178  glbconN  38236  glbconNOLD  38237  glbconxN  38238  cvrexch  38280  1cvrco  38332  1cvratex  38333  1cvrjat  38335  polval2N  38766  polsubN  38767  2polpmapN  38773  2polvalN  38774  poldmj1N  38788  pmapj2N  38789  polatN  38791  2polatN  38792  pnonsingN  38793  ispsubcl2N  38807  polsubclN  38812  poml4N  38813  pmapojoinN  38828  pl42lem1N  38839  lhpoc2N  38875  lhpocnle  38876  lhpmod2i2  38898  lhpmod6i1  38899  lhprelat3N  38900  trlcl  39024  trlle  39044  docaclN  39984  doca2N  39986  djajN  39997  dih1  40146  dih1dimatlem  40189  dochcl  40213  dochvalr3  40223  doch2val2  40224  dochss  40225  dochocss  40226  dochoc  40227  dochnoncon  40251  djhlj  40261