Theorem opoccl 36332

Description: Closure of orthocomplement operation. (choccl 29085 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 2823	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
3		opoccl.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2823	. . . . 5 ⊢ (join‘𝐾) = (join‘𝐾)
5		eqid 2823	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
6		eqid 2823	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
7		eqid 2823	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 36320	. . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
9	8	3anidm23 1417	. . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾)))
10	9	simp1d 1138	. 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))))
11	10	simp1d 1138	1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   class class class wbr 5068  ‘cfv 6357  (class class class)co 7158  Basecbs 16485  lecple 16574  occoc 16575  joincjn 17556  meetcmee 17557  0.cp0 17649  1.cp1 17650  OPcops 36310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-dm 5567  df-iota 6316  df-fv 6365  df-ov 7161  df-oposet 36314

This theorem is referenced by:  opcon2b  36335  oplecon3b  36338  oplecon1b  36339  opoc1  36340  opltcon3b  36342  opltcon1b  36343  opltcon2b  36344  riotaocN  36347  oldmm1  36355  oldmm2  36356  oldmm3N  36357  oldmm4  36358  oldmj1  36359  oldmj2  36360  oldmj3  36361  oldmj4  36362  olm11  36365  latmassOLD  36367  omllaw2N  36382  omllaw4  36384  cmtcomlemN  36386  cmt2N  36388  cmt3N  36389  cmt4N  36390  cmtbr2N  36391  cmtbr3N  36392  cmtbr4N  36393  lecmtN  36394  omlfh1N  36396  omlfh3N  36397  omlspjN  36399  cvrcon3b  36415  cvrcmp2  36422  atlatmstc  36457  glbconN  36515  glbconxN  36516  cvrexch  36558  1cvrco  36610  1cvratex  36611  1cvrjat  36613  polval2N  37044  polsubN  37045  2polpmapN  37051  2polvalN  37052  poldmj1N  37066  pmapj2N  37067  polatN  37069  2polatN  37070  pnonsingN  37071  ispsubcl2N  37085  polsubclN  37090  poml4N  37091  pmapojoinN  37106  pl42lem1N  37117  lhpoc2N  37153  lhpocnle  37154  lhpmod2i2  37176  lhpmod6i1  37177  lhprelat3N  37178  trlcl  37302  trlle  37322  docaclN  38262  doca2N  38264  djajN  38275  dih1  38424  dih1dimatlem  38467  dochcl  38491  dochvalr3  38501  doch2val2  38502  dochss  38503  dochocss  38504  dochoc  38505  dochnoncon  38529  djhlj  38539