Theorem opoccl 37215

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   class class class wbr 5075  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  lecple 16978  occoc 16979  joincjn 18038  meetcmee 18039  0.cp0 18150  1.cp1 18151  OPcops 37193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-dm 5600  df-iota 6395  df-fv 6445  df-ov 7287  df-oposet 37197

This theorem is referenced by:  opcon2b  37218  oplecon3b  37221  oplecon1b  37222  opoc1  37223  opltcon3b  37225  opltcon1b  37226  opltcon2b  37227  riotaocN  37230  oldmm1  37238  oldmm2  37239  oldmm3N  37240  oldmm4  37241  oldmj1  37242  oldmj2  37243  oldmj3  37244  oldmj4  37245  olm11  37248  latmassOLD  37250  omllaw2N  37265  omllaw4  37267  cmtcomlemN  37269  cmt2N  37271  cmt3N  37272  cmt4N  37273  cmtbr2N  37274  cmtbr3N  37275  cmtbr4N  37276  lecmtN  37277  omlfh1N  37279  omlfh3N  37280  omlspjN  37282  cvrcon3b  37298  cvrcmp2  37305  atlatmstc  37340  glbconN  37398  glbconxN  37399  cvrexch  37441  1cvrco  37493  1cvratex  37494  1cvrjat  37496  polval2N  37927  polsubN  37928  2polpmapN  37934  2polvalN  37935  poldmj1N  37949  pmapj2N  37950  polatN  37952  2polatN  37953  pnonsingN  37954  ispsubcl2N  37968  polsubclN  37973  poml4N  37974  pmapojoinN  37989  pl42lem1N  38000  lhpoc2N  38036  lhpocnle  38037  lhpmod2i2  38059  lhpmod6i1  38060  lhprelat3N  38061  trlcl  38185  trlle  38205  docaclN  39145  doca2N  39147  djajN  39158  dih1  39307  dih1dimatlem  39350  dochcl  39374  dochvalr3  39384  doch2val2  39385  dochss  39386  dochocss  39387  dochoc  39388  dochnoncon  39412  djhlj  39422