Theorem opoccl 39176

Description: Closure of orthocomplement operation. (choccl 31335 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 39164	. . . 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 395   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106   class class class wbr 5148  ‘cfv 6563  (class class class)co 7431  Basecbs 17245  lecple 17305  occoc 17306  joincjn 18369  meetcmee 18370  0.cp0 18481  1.cp1 18482  OPcops 39154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-dm 5699  df-iota 6516  df-fv 6571  df-ov 7434  df-oposet 39158

This theorem is referenced by:  opcon2b  39179  oplecon3b  39182  oplecon1b  39183  opoc1  39184  opltcon3b  39186  opltcon1b  39187  opltcon2b  39188  riotaocN  39191  oldmm1  39199  oldmm2  39200  oldmm3N  39201  oldmm4  39202  oldmj1  39203  oldmj2  39204  oldmj3  39205  oldmj4  39206  olm11  39209  latmassOLD  39211  omllaw2N  39226  omllaw4  39228  cmtcomlemN  39230  cmt2N  39232  cmt3N  39233  cmt4N  39234  cmtbr2N  39235  cmtbr3N  39236  cmtbr4N  39237  lecmtN  39238  omlfh1N  39240  omlfh3N  39241  omlspjN  39243  cvrcon3b  39259  cvrcmp2  39266  atlatmstc  39301  glbconN  39359  glbconNOLD  39360  glbconxN  39361  cvrexch  39403  1cvrco  39455  1cvratex  39456  1cvrjat  39458  polval2N  39889  polsubN  39890  2polpmapN  39896  2polvalN  39897  poldmj1N  39911  pmapj2N  39912  polatN  39914  2polatN  39915  pnonsingN  39916  ispsubcl2N  39930  polsubclN  39935  poml4N  39936  pmapojoinN  39951  pl42lem1N  39962  lhpoc2N  39998  lhpocnle  39999  lhpmod2i2  40021  lhpmod6i1  40022  lhprelat3N  40023  trlcl  40147  trlle  40167  docaclN  41107  doca2N  41109  djajN  41120  dih1  41269  dih1dimatlem  41312  dochcl  41336  dochvalr3  41346  doch2val2  41347  dochss  41348  dochocss  41349  dochoc  41350  dochnoncon  41374  djhlj  41384