Theorem opoccl 39212

Description: Closure of orthocomplement operation. (choccl 31287 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 2735	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2735	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2735	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2735	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2735	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39200	. . . 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 1540   ∈ wcel 2108   class class class wbr 5119  ‘cfv 6531  (class class class)co 7405  Basecbs 17228  lecple 17278  occoc 17279  joincjn 18323  meetcmee 18324  0.cp0 18433  1.cp1 18434  OPcops 39190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-dm 5664  df-iota 6484  df-fv 6539  df-ov 7408  df-oposet 39194

This theorem is referenced by:  opcon2b  39215  oplecon3b  39218  oplecon1b  39219  opoc1  39220  opltcon3b  39222  opltcon1b  39223  opltcon2b  39224  riotaocN  39227  oldmm1  39235  oldmm2  39236  oldmm3N  39237  oldmm4  39238  oldmj1  39239  oldmj2  39240  oldmj3  39241  oldmj4  39242  olm11  39245  latmassOLD  39247  omllaw2N  39262  omllaw4  39264  cmtcomlemN  39266  cmt2N  39268  cmt3N  39269  cmt4N  39270  cmtbr2N  39271  cmtbr3N  39272  cmtbr4N  39273  lecmtN  39274  omlfh1N  39276  omlfh3N  39277  omlspjN  39279  cvrcon3b  39295  cvrcmp2  39302  atlatmstc  39337  glbconN  39395  glbconNOLD  39396  glbconxN  39397  cvrexch  39439  1cvrco  39491  1cvratex  39492  1cvrjat  39494  polval2N  39925  polsubN  39926  2polpmapN  39932  2polvalN  39933  poldmj1N  39947  pmapj2N  39948  polatN  39950  2polatN  39951  pnonsingN  39952  ispsubcl2N  39966  polsubclN  39971  poml4N  39972  pmapojoinN  39987  pl42lem1N  39998  lhpoc2N  40034  lhpocnle  40035  lhpmod2i2  40057  lhpmod6i1  40058  lhprelat3N  40059  trlcl  40183  trlle  40203  docaclN  41143  doca2N  41145  djajN  41156  dih1  41305  dih1dimatlem  41348  dochcl  41372  dochvalr3  41382  doch2val2  41383  dochss  41384  dochocss  41385  dochoc  41386  dochnoncon  41410  djhlj  41420