Theorem opoccl 39968

Description: Closure of orthocomplement operation. (choccl 31658 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 2763	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2763	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2763	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2763	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2763	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39956	. . . 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 ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   class class class wbr 5109  ‘cfv 6536  (class class class)co 7410  Basecbs 17264  lecple 17312  occoc 17313  joincjn 18362  meetcmee 18363  0.cp0 18472  1.cp1 18473  OPcops 39946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-dm 5671  df-iota 6492  df-fv 6544  df-ov 7413  df-oposet 39950

This theorem is referenced by:  opcon2b  39971  oplecon3b  39974  oplecon1b  39975  opoc1  39976  opltcon3b  39978  opltcon1b  39979  opltcon2b  39980  riotaocN  39983  oldmm1  39991  oldmm2  39992  oldmm3N  39993  oldmm4  39994  oldmj1  39995  oldmj2  39996  oldmj3  39997  oldmj4  39998  olm11  40001  latmassOLD  40003  omllaw2N  40018  omllaw4  40020  cmtcomlemN  40022  cmt2N  40024  cmt3N  40025  cmt4N  40026  cmtbr2N  40027  cmtbr3N  40028  cmtbr4N  40029  lecmtN  40030  omlfh1N  40032  omlfh3N  40033  omlspjN  40035  cvrcon3b  40051  cvrcmp2  40058  atlatmstc  40093  glbconN  40151  glbconxN  40152  cvrexch  40194  1cvrco  40246  1cvratex  40247  1cvrjat  40249  polval2N  40680  polsubN  40681  2polpmapN  40687  2polvalN  40688  poldmj1N  40702  pmapj2N  40703  polatN  40705  2polatN  40706  pnonsingN  40707  ispsubcl2N  40721  polsubclN  40726  poml4N  40727  pmapojoinN  40742  pl42lem1N  40753  lhpoc2N  40789  lhpocnle  40790  lhpmod2i2  40812  lhpmod6i1  40813  lhprelat3N  40814  trlcl  40938  trlle  40958  docaclN  41898  doca2N  41900  djajN  41911  dih1  42060  dih1dimatlem  42103  dochcl  42127  dochvalr3  42137  doch2val2  42138  dochss  42139  dochocss  42140  dochoc  42141  dochnoncon  42165  djhlj  42175