Theorem opoccl 35772

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068   = wceq 1507   ∈ wcel 2050   class class class wbr 4929  ‘cfv 6188  (class class class)co 6976  Basecbs 16339  lecple 16428  occoc 16429  joincjn 17412  meetcmee 17413  0.cp0 17505  1.cp1 17506  OPcops 35750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751  ax-nul 5067

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3418  df-sbc 3683  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-dm 5417  df-iota 6152  df-fv 6196  df-ov 6979  df-oposet 35754

This theorem is referenced by:  opcon2b  35775  oplecon3b  35778  oplecon1b  35779  opoc1  35780  opltcon3b  35782  opltcon1b  35783  opltcon2b  35784  riotaocN  35787  oldmm1  35795  oldmm2  35796  oldmm3N  35797  oldmm4  35798  oldmj1  35799  oldmj2  35800  oldmj3  35801  oldmj4  35802  olm11  35805  latmassOLD  35807  omllaw2N  35822  omllaw4  35824  cmtcomlemN  35826  cmt2N  35828  cmt3N  35829  cmt4N  35830  cmtbr2N  35831  cmtbr3N  35832  cmtbr4N  35833  lecmtN  35834  omlfh1N  35836  omlfh3N  35837  omlspjN  35839  cvrcon3b  35855  cvrcmp2  35862  atlatmstc  35897  glbconN  35955  glbconxN  35956  cvrexch  35998  1cvrco  36050  1cvratex  36051  1cvrjat  36053  polval2N  36484  polsubN  36485  2polpmapN  36491  2polvalN  36492  poldmj1N  36506  pmapj2N  36507  polatN  36509  2polatN  36510  pnonsingN  36511  ispsubcl2N  36525  polsubclN  36530  poml4N  36531  pmapojoinN  36546  pl42lem1N  36557  lhpoc2N  36593  lhpocnle  36594  lhpmod2i2  36616  lhpmod6i1  36617  lhprelat3N  36618  trlcl  36742  trlle  36762  docaclN  37702  doca2N  37704  djajN  37715  dih1  37864  dih1dimatlem  37907  dochcl  37931  dochvalr3  37941  doch2val2  37942  dochss  37943  dochocss  37944  dochoc  37945  dochnoncon  37969  djhlj  37979