Theorem opoccl 39454

Description: Closure of orthocomplement operation. (choccl 31381 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 2736	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2736	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2736	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2736	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2736	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39442	. . . 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 5098  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  lecple 17184  occoc 17185  joincjn 18234  meetcmee 18235  0.cp0 18344  1.cp1 18345  OPcops 39432

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 2708  ax-nul 5251

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-dm 5634  df-iota 6448  df-fv 6500  df-ov 7361  df-oposet 39436

This theorem is referenced by:  opcon2b  39457  oplecon3b  39460  oplecon1b  39461  opoc1  39462  opltcon3b  39464  opltcon1b  39465  opltcon2b  39466  riotaocN  39469  oldmm1  39477  oldmm2  39478  oldmm3N  39479  oldmm4  39480  oldmj1  39481  oldmj2  39482  oldmj3  39483  oldmj4  39484  olm11  39487  latmassOLD  39489  omllaw2N  39504  omllaw4  39506  cmtcomlemN  39508  cmt2N  39510  cmt3N  39511  cmt4N  39512  cmtbr2N  39513  cmtbr3N  39514  cmtbr4N  39515  lecmtN  39516  omlfh1N  39518  omlfh3N  39519  omlspjN  39521  cvrcon3b  39537  cvrcmp2  39544  atlatmstc  39579  glbconN  39637  glbconxN  39638  cvrexch  39680  1cvrco  39732  1cvratex  39733  1cvrjat  39735  polval2N  40166  polsubN  40167  2polpmapN  40173  2polvalN  40174  poldmj1N  40188  pmapj2N  40189  polatN  40191  2polatN  40192  pnonsingN  40193  ispsubcl2N  40207  polsubclN  40212  poml4N  40213  pmapojoinN  40228  pl42lem1N  40239  lhpoc2N  40275  lhpocnle  40276  lhpmod2i2  40298  lhpmod6i1  40299  lhprelat3N  40300  trlcl  40424  trlle  40444  docaclN  41384  doca2N  41386  djajN  41397  dih1  41546  dih1dimatlem  41589  dochcl  41613  dochvalr3  41623  doch2val2  41624  dochss  41625  dochocss  41626  dochoc  41627  dochnoncon  41651  djhlj  41661