Theorem opoccl 39150

Description: Closure of orthocomplement operation. (choccl 31338 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 2740	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2740	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2740	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2740	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2740	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39138	. . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
9	8	3anidm23 1421	. . 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 1087   = wceq 1537   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  lecple 17318  occoc 17319  joincjn 18381  meetcmee 18382  0.cp0 18493  1.cp1 18494  OPcops 39128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-dm 5710  df-iota 6525  df-fv 6581  df-ov 7451  df-oposet 39132

This theorem is referenced by:  opcon2b  39153  oplecon3b  39156  oplecon1b  39157  opoc1  39158  opltcon3b  39160  opltcon1b  39161  opltcon2b  39162  riotaocN  39165  oldmm1  39173  oldmm2  39174  oldmm3N  39175  oldmm4  39176  oldmj1  39177  oldmj2  39178  oldmj3  39179  oldmj4  39180  olm11  39183  latmassOLD  39185  omllaw2N  39200  omllaw4  39202  cmtcomlemN  39204  cmt2N  39206  cmt3N  39207  cmt4N  39208  cmtbr2N  39209  cmtbr3N  39210  cmtbr4N  39211  lecmtN  39212  omlfh1N  39214  omlfh3N  39215  omlspjN  39217  cvrcon3b  39233  cvrcmp2  39240  atlatmstc  39275  glbconN  39333  glbconNOLD  39334  glbconxN  39335  cvrexch  39377  1cvrco  39429  1cvratex  39430  1cvrjat  39432  polval2N  39863  polsubN  39864  2polpmapN  39870  2polvalN  39871  poldmj1N  39885  pmapj2N  39886  polatN  39888  2polatN  39889  pnonsingN  39890  ispsubcl2N  39904  polsubclN  39909  poml4N  39910  pmapojoinN  39925  pl42lem1N  39936  lhpoc2N  39972  lhpocnle  39973  lhpmod2i2  39995  lhpmod6i1  39996  lhprelat3N  39997  trlcl  40121  trlle  40141  docaclN  41081  doca2N  41083  djajN  41094  dih1  41243  dih1dimatlem  41286  dochcl  41310  dochvalr3  41320  doch2val2  41321  dochss  41322  dochocss  41323  dochoc  41324  dochnoncon  41348  djhlj  41358