Theorem opoccl 36945

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110   class class class wbr 5053  ‘cfv 6380  (class class class)co 7213  Basecbs 16760  lecple 16809  occoc 16810  joincjn 17818  meetcmee 17819  0.cp0 17929  1.cp1 17930  OPcops 36923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-nul 5199

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-dm 5561  df-iota 6338  df-fv 6388  df-ov 7216  df-oposet 36927

This theorem is referenced by:  opcon2b  36948  oplecon3b  36951  oplecon1b  36952  opoc1  36953  opltcon3b  36955  opltcon1b  36956  opltcon2b  36957  riotaocN  36960  oldmm1  36968  oldmm2  36969  oldmm3N  36970  oldmm4  36971  oldmj1  36972  oldmj2  36973  oldmj3  36974  oldmj4  36975  olm11  36978  latmassOLD  36980  omllaw2N  36995  omllaw4  36997  cmtcomlemN  36999  cmt2N  37001  cmt3N  37002  cmt4N  37003  cmtbr2N  37004  cmtbr3N  37005  cmtbr4N  37006  lecmtN  37007  omlfh1N  37009  omlfh3N  37010  omlspjN  37012  cvrcon3b  37028  cvrcmp2  37035  atlatmstc  37070  glbconN  37128  glbconxN  37129  cvrexch  37171  1cvrco  37223  1cvratex  37224  1cvrjat  37226  polval2N  37657  polsubN  37658  2polpmapN  37664  2polvalN  37665  poldmj1N  37679  pmapj2N  37680  polatN  37682  2polatN  37683  pnonsingN  37684  ispsubcl2N  37698  polsubclN  37703  poml4N  37704  pmapojoinN  37719  pl42lem1N  37730  lhpoc2N  37766  lhpocnle  37767  lhpmod2i2  37789  lhpmod6i1  37790  lhprelat3N  37791  trlcl  37915  trlle  37935  docaclN  38875  doca2N  38877  djajN  38888  dih1  39037  dih1dimatlem  39080  dochcl  39104  dochvalr3  39114  doch2val2  39115  dochss  39116  dochocss  39117  dochoc  39118  dochnoncon  39142  djhlj  39152