Theorem opoccl 40026

Description: Closure of orthocomplement operation. (choccl 31729 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 2765	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2765	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2765	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2765	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2765	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 40014	. . . 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 2146   class class class wbr 5111  ‘cfv 6540  (class class class)co 7419  Basecbs 17291  lecple 17339  occoc 17340  joincjn 18389  meetcmee 18390  0.cp0 18499  1.cp1 18500  OPcops 40004

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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6496  df-fv 6548  df-ov 7422  df-oposet 40008

This theorem is used by:  opcon2b  40029  oplecon3b  40032  oplecon1b  40033  opoc1  40034  opltcon3b  40036  opltcon1b  40037  opltcon2b  40038  riotaocN  40041  oldmm1  40049  oldmm2  40050  oldmm3N  40051  oldmm4  40052  oldmj1  40053  oldmj2  40054  oldmj3  40055  oldmj4  40056  olm11  40059  latmassOLD  40061  omllaw2N  40076  omllaw4  40078  cmtcomlemN  40080  cmt2N  40082  cmt3N  40083  cmt4N  40084  cmtbr2N  40085  cmtbr3N  40086  cmtbr4N  40087  lecmtN  40088  omlfh1N  40090  omlfh3N  40091  omlspjN  40093  cvrcon3b  40109  cvrcmp2  40116  atlatmstc  40151  glbconN  40209  glbconxN  40210  cvrexch  40252  1cvrco  40304  1cvratex  40305  1cvrjat  40307  polval2N  40738  polsubN  40739  2polpmapN  40745  2polvalN  40746  poldmj1N  40760  pmapj2N  40761  polatN  40763  2polatN  40764  pnonsingN  40765  ispsubcl2N  40779  polsubclN  40784  poml4N  40785  pmapojoinN  40800  pl42lem1N  40811  lhpoc2N  40847  lhpocnle  40848  lhpmod2i2  40870  lhpmod6i1  40871  lhprelat3N  40872  trlcl  40996  trlle  41016  docaclN  41956  doca2N  41958  djajN  41969  dih1  42118  dih1dimatlem  42161  dochcl  42185  dochvalr3  42195  doch2val2  42196  dochss  42197  dochocss  42198  dochoc  42199  dochnoncon  42223  djhlj  42233