Theorem opoccl 39996

Description: Closure of orthocomplement operation. (choccl 31667 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 39984	. . . 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 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   class class class wbr 5109  ‘cfv 6536  (class class class)co 7410  Basecbs 17273  lecple 17321  occoc 17322  joincjn 18371  meetcmee 18372  0.cp0 18481  1.cp1 18482  OPcops 39974

This proof depends on 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 proof 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 39978

This theorem is used by:  opcon2b  39999  oplecon3b  40002  oplecon1b  40003  opoc1  40004  opltcon3b  40006  opltcon1b  40007  opltcon2b  40008  riotaocN  40011  oldmm1  40019  oldmm2  40020  oldmm3N  40021  oldmm4  40022  oldmj1  40023  oldmj2  40024  oldmj3  40025  oldmj4  40026  olm11  40029  latmassOLD  40031  omllaw2N  40046  omllaw4  40048  cmtcomlemN  40050  cmt2N  40052  cmt3N  40053  cmt4N  40054  cmtbr2N  40055  cmtbr3N  40056  cmtbr4N  40057  lecmtN  40058  omlfh1N  40060  omlfh3N  40061  omlspjN  40063  cvrcon3b  40079  cvrcmp2  40086  atlatmstc  40121  glbconN  40179  glbconxN  40180  cvrexch  40222  1cvrco  40274  1cvratex  40275  1cvrjat  40277  polval2N  40708  polsubN  40709  2polpmapN  40715  2polvalN  40716  poldmj1N  40730  pmapj2N  40731  polatN  40733  2polatN  40734  pnonsingN  40735  ispsubcl2N  40749  polsubclN  40754  poml4N  40755  pmapojoinN  40770  pl42lem1N  40781  lhpoc2N  40817  lhpocnle  40818  lhpmod2i2  40840  lhpmod6i1  40841  lhprelat3N  40842  trlcl  40966  trlle  40986  docaclN  41926  doca2N  41928  djajN  41939  dih1  42088  dih1dimatlem  42131  dochcl  42155  dochvalr3  42165  doch2val2  42166  dochss  42167  dochocss  42168  dochoc  42169  dochnoncon  42193  djhlj  42203