Theorem opoccl 40068

Description: Closure of orthocomplement operation. (choccl 31788 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 2760	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2760	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2760	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2760	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2760	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 40056	. . . 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 6533  (class class class)co 7414  Basecbs 17302  lecple 17350  occoc 17351  joincjn 18400  meetcmee 18401  0.cp0 18510  1.cp1 18511  OPcops 40046

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 2732  ax-nul 5263

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  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 5665  df-iota 6489  df-fv 6541  df-ov 7417  df-oposet 40050

This theorem is used by:  opcon2b  40071  oplecon3b  40074  oplecon1b  40075  opoc1  40076  opltcon3b  40078  opltcon1b  40079  opltcon2b  40080  riotaocN  40083  oldmm1  40091  oldmm2  40092  oldmm3N  40093  oldmm4  40094  oldmj1  40095  oldmj2  40096  oldmj3  40097  oldmj4  40098  olm11  40101  latmassOLD  40103  omllaw2N  40118  omllaw4  40120  cmtcomlemN  40122  cmt2N  40124  cmt3N  40125  cmt4N  40126  cmtbr2N  40127  cmtbr3N  40128  cmtbr4N  40129  lecmtN  40130  omlfh1N  40132  omlfh3N  40133  omlspjN  40135  cvrcon3b  40151  cvrcmp2  40158  atlatmstc  40193  glbconN  40251  glbconxN  40252  cvrexch  40294  1cvrco  40346  1cvratex  40347  1cvrjat  40349  polval2N  40780  polsubN  40781  2polpmapN  40787  2polvalN  40788  poldmj1N  40802  pmapj2N  40803  polatN  40805  2polatN  40806  pnonsingN  40807  ispsubcl2N  40821  polsubclN  40826  poml4N  40827  pmapojoinN  40842  pl42lem1N  40853  lhpoc2N  40889  lhpocnle  40890  lhpmod2i2  40912  lhpmod6i1  40913  lhprelat3N  40914  trlcl  41038  trlle  41058  docaclN  41998  doca2N  42000  djajN  42011  dih1  42160  dih1dimatlem  42203  dochcl  42227  dochvalr3  42237  doch2val2  42238  dochss  42239  dochocss  42240  dochoc  42241  dochnoncon  42265  djhlj  42275