Theorem opoccl 34653

Description: Closure of orthocomplement operation. (choccl 26096 analog.) (Contributed by NM, 20-Oct-2011.)

Hypotheses

Ref	Expression
opoccl.b	|- B = ( Base ` K )
opoccl.o	|- ._|_ = ( oc ` K )

Assertion

Ref	Expression
opoccl	|- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )

Proof of Theorem opoccl

Step	Hyp	Ref	Expression
1		opoccl.b	. . . . 5 |- B = ( Base ` K )
2		eqid 2443	. . . . 5 |- ( le ` K ) = ( le ` K )
3		opoccl.o	. . . . 5 |- ._|_ = ( oc ` K )
4		eqid 2443	. . . . 5 |- ( join ` K ) = ( join ` K )
5		eqid 2443	. . . . 5 |- ( meet ` K ) = ( meet ` K )
6		eqid 2443	. . . . 5 |- ( 0. ` K ) = ( 0. ` K )
7		eqid 2443	. . . . 5 |- ( 1. ` K ) = ( 1. ` K )
8	1, 2, 3, 4, 5, 6, 7	oposlem 34641	. . . 4 |- ( ( K e. OP /\ X e. B /\ X e. B ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X ( le ` K ) X -> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` X ) ) ) /\ ( X ( join ` K ) ( ._|_ ` X ) ) = ( 1. ` K ) /\ ( X ( meet ` K ) ( ._|_ ` X ) ) = ( 0. ` K ) ) )
9	8	3anidm23 1288	. . 3 |- ( ( K e. OP /\ X e. B ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X ( le ` K ) X -> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` X ) ) ) /\ ( X ( join ` K ) ( ._|_ ` X ) ) = ( 1. ` K ) /\ ( X ( meet ` K ) ( ._|_ ` X ) ) = ( 0. ` K ) ) )
10	9	simp1d 1009	. 2 |- ( ( K e. OP /\ X e. B ) -> ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X ( le ` K ) X -> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` X ) ) ) )
11	10	simp1d 1009	1 |- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 974   = wceq 1383   e. wcel 1804   class class class wbr 4437   ` cfv 5578  (class class class)co 6281   Basecbs 14509   lecple 14581   occoc 14582   joincjn 15447   meetcmee 15448   0.cp0 15541   1.cp1 15542   OPcops 34631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-nul 4566

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-dm 4999  df-iota 5541  df-fv 5586  df-ov 6284  df-oposet 34635

This theorem is referenced by:  opcon2b  34656  oplecon3b  34659  oplecon1b  34660  opoc1  34661  opltcon3b  34663  opltcon1b  34664  opltcon2b  34665  riotaocN  34668  oldmm1  34676  oldmm2  34677  oldmm3N  34678  oldmm4  34679  oldmj1  34680  oldmj2  34681  oldmj3  34682  oldmj4  34683  olm11  34686  latmassOLD  34688  omllaw2N  34703  omllaw4  34705  cmtcomlemN  34707  cmt2N  34709  cmt3N  34710  cmt4N  34711  cmtbr2N  34712  cmtbr3N  34713  cmtbr4N  34714  lecmtN  34715  omlfh1N  34717  omlfh3N  34718  omlspjN  34720  cvrcon3b  34736  cvrcmp2  34743  atlatmstc  34778  glbconN  34835  glbconxN  34836  cvrexch  34878  1cvrco  34930  1cvratex  34931  1cvrjat  34933  polval2N  35364  polsubN  35365  2polpmapN  35371  2polvalN  35372  poldmj1N  35386  pmapj2N  35387  polatN  35389  2polatN  35390  pnonsingN  35391  ispsubcl2N  35405  polsubclN  35410  poml4N  35411  pmapojoinN  35426  pl42lem1N  35437  lhpoc2N  35473  lhpocnle  35474  lhpmod2i2  35496  lhpmod6i1  35497  lhprelat3N  35498  trlcl  35623  trlle  35643  docaclN  36585  doca2N  36587  djajN  36598  dih1  36747  dih1dimatlem  36790  dochcl  36814  dochvalr3  36824  doch2val2  36825  dochss  36826  dochocss  36827  dochoc  36828  dochnoncon  36852  djhlj  36862