Theorem opoccl 40251

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  lecple 17435  occoc 17436  joincjn 18485  meetcmee 18486  0.cp0 18595  1.cp1 18596  OPcops 40229

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5661  df-iota 6494  df-fv 6546  df-ov 7423  df-oposet 40233

This theorem is used by:  opcon2b  40254  oplecon3b  40257  oplecon1b  40258  opoc1  40259  opltcon3b  40261  opltcon1b  40262  opltcon2b  40263  riotaocN  40266  oldmm1  40274  oldmm2  40275  oldmm3N  40276  oldmm4  40277  oldmj1  40278  oldmj2  40279  oldmj3  40280  oldmj4  40281  olm11  40284  latmassOLD  40286  omllaw2N  40301  omllaw4  40303  cmtcomlemN  40305  cmt2N  40307  cmt3N  40308  cmt4N  40309  cmtbr2N  40310  cmtbr3N  40311  cmtbr4N  40312  lecmtN  40313  omlfh1N  40315  omlfh3N  40316  omlspjN  40318  cvrcon3b  40334  cvrcmp2  40341  atlatmstc  40376  glbconN  40434  glbconxN  40435  cvrexch  40477  1cvrco  40529  1cvratex  40530  1cvrjat  40532  polval2N  40963  polsubN  40964  2polpmapN  40970  2polvalN  40971  poldmj1N  40985  pmapj2N  40986  polatN  40988  2polatN  40989  pnonsingN  40990  ispsubcl2N  41004  polsubclN  41009  poml4N  41010  pmapojoinN  41025  pl42lem1N  41036  lhpoc2N  41072  lhpocnle  41073  lhpmod2i2  41095  lhpmod6i1  41096  lhprelat3N  41097  trlcl  41221  trlle  41241  docaclN  42181  doca2N  42183  djajN  42194  dih1  42343  dih1dimatlem  42386  dochcl  42410  dochvalr3  42420  doch2val2  42421  dochss  42422  dochocss  42423  dochoc  42424  dochnoncon  42448  djhlj  42458