Theorem opoccl 40388

Description: Closure of orthocomplement operation. (choccl 31917 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 40376	. . . 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 1569   ∈ wcel 2144   class class class wbr 5102  ‘cfv 6543  (class class class)co 7424  Basecbs 17396  lecple 17444  occoc 17445  joincjn 18494  meetcmee 18495  0.cp0 18604  1.cp1 18605  OPcops 40366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-dm 5661  df-iota 6497  df-fv 6551  df-ov 7427  df-oposet 40370

This theorem is used by:  opcon2b  40391  oplecon3b  40394  oplecon1b  40395  opoc1  40396  opltcon3b  40398  opltcon1b  40399  opltcon2b  40400  riotaocN  40403  oldmm1  40411  oldmm2  40412  oldmm3N  40413  oldmm4  40414  oldmj1  40415  oldmj2  40416  oldmj3  40417  oldmj4  40418  olm11  40421  latmassOLD  40423  omllaw2N  40438  omllaw4  40440  cmtcomlemN  40442  cmt2N  40444  cmt3N  40445  cmt4N  40446  cmtbr2N  40447  cmtbr3N  40448  cmtbr4N  40449  lecmtN  40450  omlfh1N  40452  omlfh3N  40453  omlspjN  40455  cvrcon3b  40471  cvrcmp2  40478  atlatmstc  40513  glbconN  40571  glbconxN  40572  cvrexch  40614  1cvrco  40666  1cvratex  40667  1cvrjat  40669  polval2N  41100  polsubN  41101  2polpmapN  41107  2polvalN  41108  poldmj1N  41122  pmapj2N  41123  polatN  41125  2polatN  41126  pnonsingN  41127  ispsubcl2N  41141  polsubclN  41146  poml4N  41147  pmapojoinN  41162  pl42lem1N  41173  lhpoc2N  41209  lhpocnle  41210  lhpmod2i2  41232  lhpmod6i1  41233  lhprelat3N  41234  trlcl  41358  trlle  41378  docaclN  42318  doca2N  42320  djajN  42331  dih1  42480  dih1dimatlem  42523  dochcl  42547  dochvalr3  42557  doch2val2  42558  dochss  42559  dochocss  42560  dochoc  42561  dochnoncon  42585  djhlj  42595