Theorem opoccl 32679

Description: Closure of orthocomplement operation. (choccl 26945 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 2422	. . . . 5 |- ( le ` K ) = ( le ` K )
3		opoccl.o	. . . . 5 |- ._|_ = ( oc ` K )
4		eqid 2422	. . . . 5 |- ( join ` K ) = ( join ` K )
5		eqid 2422	. . . . 5 |- ( meet ` K ) = ( meet ` K )
6		eqid 2422	. . . . 5 |- ( 0. ` K ) = ( 0. ` K )
7		eqid 2422	. . . . 5 |- ( 1. ` K ) = ( 1. ` K )
8	1, 2, 3, 4, 5, 6, 7	oposlem 32667	. . . 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 1323	. . 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 1017	. 2 |- ( ( K e. OP /\ X e. B ) -> ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X ( le ` K ) X -> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` X ) ) ) )
11	10	simp1d 1017	1 |- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1868   class class class wbr 4420   ` cfv 5598  (class class class)co 6302   Basecbs 15109   lecple 15185   occoc 15186   joincjn 16177   meetcmee 16178   0.cp0 16271   1.cp1 16272   OPcops 32657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-nul 4552

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-dm 4860  df-iota 5562  df-fv 5606  df-ov 6305  df-oposet 32661

This theorem is referenced by:  opcon2b  32682  oplecon3b  32685  oplecon1b  32686  opoc1  32687  opltcon3b  32689  opltcon1b  32690  opltcon2b  32691  riotaocN  32694  oldmm1  32702  oldmm2  32703  oldmm3N  32704  oldmm4  32705  oldmj1  32706  oldmj2  32707  oldmj3  32708  oldmj4  32709  olm11  32712  latmassOLD  32714  omllaw2N  32729  omllaw4  32731  cmtcomlemN  32733  cmt2N  32735  cmt3N  32736  cmt4N  32737  cmtbr2N  32738  cmtbr3N  32739  cmtbr4N  32740  lecmtN  32741  omlfh1N  32743  omlfh3N  32744  omlspjN  32746  cvrcon3b  32762  cvrcmp2  32769  atlatmstc  32804  glbconN  32861  glbconxN  32862  cvrexch  32904  1cvrco  32956  1cvratex  32957  1cvrjat  32959  polval2N  33390  polsubN  33391  2polpmapN  33397  2polvalN  33398  poldmj1N  33412  pmapj2N  33413  polatN  33415  2polatN  33416  pnonsingN  33417  ispsubcl2N  33431  polsubclN  33436  poml4N  33437  pmapojoinN  33452  pl42lem1N  33463  lhpoc2N  33499  lhpocnle  33500  lhpmod2i2  33522  lhpmod6i1  33523  lhprelat3N  33524  trlcl  33649  trlle  33669  docaclN  34611  doca2N  34613  djajN  34624  dih1  34773  dih1dimatlem  34816  dochcl  34840  dochvalr3  34850  doch2val2  34851  dochss  34852  dochocss  34853  dochoc  34854  dochnoncon  34878  djhlj  34888