Theorem opoccl 39640

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   class class class wbr 5085  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  lecple 17227  occoc 17228  joincjn 18277  meetcmee 18278  0.cp0 18387  1.cp1 18388  OPcops 39618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-dm 5641  df-iota 6454  df-fv 6506  df-ov 7370  df-oposet 39622

This theorem is referenced by:  opcon2b  39643  oplecon3b  39646  oplecon1b  39647  opoc1  39648  opltcon3b  39650  opltcon1b  39651  opltcon2b  39652  riotaocN  39655  oldmm1  39663  oldmm2  39664  oldmm3N  39665  oldmm4  39666  oldmj1  39667  oldmj2  39668  oldmj3  39669  oldmj4  39670  olm11  39673  latmassOLD  39675  omllaw2N  39690  omllaw4  39692  cmtcomlemN  39694  cmt2N  39696  cmt3N  39697  cmt4N  39698  cmtbr2N  39699  cmtbr3N  39700  cmtbr4N  39701  lecmtN  39702  omlfh1N  39704  omlfh3N  39705  omlspjN  39707  cvrcon3b  39723  cvrcmp2  39730  atlatmstc  39765  glbconN  39823  glbconxN  39824  cvrexch  39866  1cvrco  39918  1cvratex  39919  1cvrjat  39921  polval2N  40352  polsubN  40353  2polpmapN  40359  2polvalN  40360  poldmj1N  40374  pmapj2N  40375  polatN  40377  2polatN  40378  pnonsingN  40379  ispsubcl2N  40393  polsubclN  40398  poml4N  40399  pmapojoinN  40414  pl42lem1N  40425  lhpoc2N  40461  lhpocnle  40462  lhpmod2i2  40484  lhpmod6i1  40485  lhprelat3N  40486  trlcl  40610  trlle  40630  docaclN  41570  doca2N  41572  djajN  41583  dih1  41732  dih1dimatlem  41775  dochcl  41799  dochvalr3  41809  doch2val2  41810  dochss  41811  dochocss  41812  dochoc  41813  dochnoncon  41837  djhlj  41847