Theorem opoccl 39857

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   class class class wbr 5113  ‘cfv 6537  (class class class)co 7411  Basecbs 17268  lecple 17316  occoc 17317  joincjn 18366  meetcmee 18367  0.cp0 18476  1.cp1 18477  OPcops 39835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-dm 5672  df-iota 6493  df-fv 6545  df-ov 7414  df-oposet 39839

This theorem is referenced by:  opcon2b  39860  oplecon3b  39863  oplecon1b  39864  opoc1  39865  opltcon3b  39867  opltcon1b  39868  opltcon2b  39869  riotaocN  39872  oldmm1  39880  oldmm2  39881  oldmm3N  39882  oldmm4  39883  oldmj1  39884  oldmj2  39885  oldmj3  39886  oldmj4  39887  olm11  39890  latmassOLD  39892  omllaw2N  39907  omllaw4  39909  cmtcomlemN  39911  cmt2N  39913  cmt3N  39914  cmt4N  39915  cmtbr2N  39916  cmtbr3N  39917  cmtbr4N  39918  lecmtN  39919  omlfh1N  39921  omlfh3N  39922  omlspjN  39924  cvrcon3b  39940  cvrcmp2  39947  atlatmstc  39982  glbconN  40040  glbconxN  40041  cvrexch  40083  1cvrco  40135  1cvratex  40136  1cvrjat  40138  polval2N  40569  polsubN  40570  2polpmapN  40576  2polvalN  40577  poldmj1N  40591  pmapj2N  40592  polatN  40594  2polatN  40595  pnonsingN  40596  ispsubcl2N  40610  polsubclN  40615  poml4N  40616  pmapojoinN  40631  pl42lem1N  40642  lhpoc2N  40678  lhpocnle  40679  lhpmod2i2  40701  lhpmod6i1  40702  lhprelat3N  40703  trlcl  40827  trlle  40847  docaclN  41787  doca2N  41789  djajN  41800  dih1  41949  dih1dimatlem  41992  dochcl  42016  dochvalr3  42026  doch2val2  42027  dochss  42028  dochocss  42029  dochoc  42030  dochnoncon  42054  djhlj  42064