Theorem opoccl 39818

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142   class class class wbr 5100  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  lecple 17293  occoc 17294  joincjn 18343  meetcmee 18344  0.cp0 18453  1.cp1 18454  OPcops 39796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5256

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5657  df-iota 6477  df-fv 6529  df-ov 7399  df-oposet 39800

This theorem is referenced by:  opcon2b  39821  oplecon3b  39824  oplecon1b  39825  opoc1  39826  opltcon3b  39828  opltcon1b  39829  opltcon2b  39830  riotaocN  39833  oldmm1  39841  oldmm2  39842  oldmm3N  39843  oldmm4  39844  oldmj1  39845  oldmj2  39846  oldmj3  39847  oldmj4  39848  olm11  39851  latmassOLD  39853  omllaw2N  39868  omllaw4  39870  cmtcomlemN  39872  cmt2N  39874  cmt3N  39875  cmt4N  39876  cmtbr2N  39877  cmtbr3N  39878  cmtbr4N  39879  lecmtN  39880  omlfh1N  39882  omlfh3N  39883  omlspjN  39885  cvrcon3b  39901  cvrcmp2  39908  atlatmstc  39943  glbconN  40001  glbconxN  40002  cvrexch  40044  1cvrco  40096  1cvratex  40097  1cvrjat  40099  polval2N  40530  polsubN  40531  2polpmapN  40537  2polvalN  40538  poldmj1N  40552  pmapj2N  40553  polatN  40555  2polatN  40556  pnonsingN  40557  ispsubcl2N  40571  polsubclN  40576  poml4N  40577  pmapojoinN  40592  pl42lem1N  40603  lhpoc2N  40639  lhpocnle  40640  lhpmod2i2  40662  lhpmod6i1  40663  lhprelat3N  40664  trlcl  40788  trlle  40808  docaclN  41748  doca2N  41750  djajN  41761  dih1  41910  dih1dimatlem  41953  dochcl  41977  dochvalr3  41987  doch2val2  41988  dochss  41989  dochocss  41990  dochoc  41991  dochnoncon  42015  djhlj  42025