Theorem opoccl 39177

Description: Closure of orthocomplement operation. (choccl 31250 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 2729	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2729	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2729	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2729	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2729	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39165	. . . 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 2109   class class class wbr 5092  ‘cfv 6482  (class class class)co 7349  Basecbs 17120  lecple 17168  occoc 17169  joincjn 18217  meetcmee 18218  0.cp0 18327  1.cp1 18328  OPcops 39155

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-dm 5629  df-iota 6438  df-fv 6490  df-ov 7352  df-oposet 39159

This theorem is referenced by:  opcon2b  39180  oplecon3b  39183  oplecon1b  39184  opoc1  39185  opltcon3b  39187  opltcon1b  39188  opltcon2b  39189  riotaocN  39192  oldmm1  39200  oldmm2  39201  oldmm3N  39202  oldmm4  39203  oldmj1  39204  oldmj2  39205  oldmj3  39206  oldmj4  39207  olm11  39210  latmassOLD  39212  omllaw2N  39227  omllaw4  39229  cmtcomlemN  39231  cmt2N  39233  cmt3N  39234  cmt4N  39235  cmtbr2N  39236  cmtbr3N  39237  cmtbr4N  39238  lecmtN  39239  omlfh1N  39241  omlfh3N  39242  omlspjN  39244  cvrcon3b  39260  cvrcmp2  39267  atlatmstc  39302  glbconN  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