Theorem opoccl 39180

Description: Closure of orthocomplement operation. (choccl 31285 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 2729	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2729	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2729	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2729	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2729	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39168	. . . 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 1540   ∈ wcel 2109   class class class wbr 5102  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  lecple 17203  occoc 17204  joincjn 18252  meetcmee 18253  0.cp0 18362  1.cp1 18363  OPcops 39158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507  df-ov 7372  df-oposet 39162

This theorem is referenced by:  opcon2b  39183  oplecon3b  39186  oplecon1b  39187  opoc1  39188  opltcon3b  39190  opltcon1b  39191  opltcon2b  39192  riotaocN  39195  oldmm1  39203  oldmm2  39204  oldmm3N  39205  oldmm4  39206  oldmj1  39207  oldmj2  39208  oldmj3  39209  oldmj4  39210  olm11  39213  latmassOLD  39215  omllaw2N  39230  omllaw4  39232  cmtcomlemN  39234  cmt2N  39236  cmt3N  39237  cmt4N  39238  cmtbr2N  39239  cmtbr3N  39240  cmtbr4N  39241  lecmtN  39242  omlfh1N  39244  omlfh3N  39245  omlspjN  39247  cvrcon3b  39263  cvrcmp2  39270  atlatmstc  39305  glbconN  39363  glbconNOLD  39364  glbconxN  39365  cvrexch  39407  1cvrco  39459  1cvratex  39460  1cvrjat  39462  polval2N  39893  polsubN  39894  2polpmapN  39900  2polvalN  39901  poldmj1N  39915  pmapj2N  39916  polatN  39918  2polatN  39919  pnonsingN  39920  ispsubcl2N  39934  polsubclN  39939  poml4N  39940  pmapojoinN  39955  pl42lem1N  39966  lhpoc2N  40002  lhpocnle  40003  lhpmod2i2  40025  lhpmod6i1  40026  lhprelat3N  40027  trlcl  40151  trlle  40171  docaclN  41111  doca2N  41113  djajN  41124  dih1  41273  dih1dimatlem  41316  dochcl  41340  dochvalr3  41350  doch2val2  41351  dochss  41352  dochocss  41353  dochoc  41354  dochnoncon  41378  djhlj  41388