Theorem opoccl 39187

Description: Closure of orthocomplement operation. (choccl 31235 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 39175	. . . 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 5107  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  lecple 17227  occoc 17228  joincjn 18272  meetcmee 18273  0.cp0 18382  1.cp1 18383  OPcops 39165

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 5261

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-dm 5648  df-iota 6464  df-fv 6519  df-ov 7390  df-oposet 39169

This theorem is referenced by:  opcon2b  39190  oplecon3b  39193  oplecon1b  39194  opoc1  39195  opltcon3b  39197  opltcon1b  39198  opltcon2b  39199  riotaocN  39202  oldmm1  39210  oldmm2  39211  oldmm3N  39212  oldmm4  39213  oldmj1  39214  oldmj2  39215  oldmj3  39216  oldmj4  39217  olm11  39220  latmassOLD  39222  omllaw2N  39237  omllaw4  39239  cmtcomlemN  39241  cmt2N  39243  cmt3N  39244  cmt4N  39245  cmtbr2N  39246  cmtbr3N  39247  cmtbr4N  39248  lecmtN  39249  omlfh1N  39251  omlfh3N  39252  omlspjN  39254  cvrcon3b  39270  cvrcmp2  39277  atlatmstc  39312  glbconN  39370  glbconNOLD  39371  glbconxN  39372  cvrexch  39414  1cvrco  39466  1cvratex  39467  1cvrjat  39469  polval2N  39900  polsubN  39901  2polpmapN  39907  2polvalN  39908  poldmj1N  39922  pmapj2N  39923  polatN  39925  2polatN  39926  pnonsingN  39927  ispsubcl2N  39941  polsubclN  39946  poml4N  39947  pmapojoinN  39962  pl42lem1N  39973  lhpoc2N  40009  lhpocnle  40010  lhpmod2i2  40032  lhpmod6i1  40033  lhprelat3N  40034  trlcl  40158  trlle  40178  docaclN  41118  doca2N  41120  djajN  41131  dih1  41280  dih1dimatlem  41323  dochcl  41347  dochvalr3  41357  doch2val2  41358  dochss  41359  dochocss  41360  dochoc  41361  dochnoncon  41385  djhlj  41395