Theorem opoccl 33961

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   class class class wbr 4613  ‘cfv 5847  (class class class)co 6604  Basecbs 15781  lecple 15869  occoc 15870  joincjn 16865  meetcmee 16866  0.cp0 16958  1.cp1 16959  OPcops 33939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4749

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-dm 5084  df-iota 5810  df-fv 5855  df-ov 6607  df-oposet 33943

This theorem is referenced by:  opcon2b  33964  oplecon3b  33967  oplecon1b  33968  opoc1  33969  opltcon3b  33971  opltcon1b  33972  opltcon2b  33973  riotaocN  33976  oldmm1  33984  oldmm2  33985  oldmm3N  33986  oldmm4  33987  oldmj1  33988  oldmj2  33989  oldmj3  33990  oldmj4  33991  olm11  33994  latmassOLD  33996  omllaw2N  34011  omllaw4  34013  cmtcomlemN  34015  cmt2N  34017  cmt3N  34018  cmt4N  34019  cmtbr2N  34020  cmtbr3N  34021  cmtbr4N  34022  lecmtN  34023  omlfh1N  34025  omlfh3N  34026  omlspjN  34028  cvrcon3b  34044  cvrcmp2  34051  atlatmstc  34086  glbconN  34143  glbconxN  34144  cvrexch  34186  1cvrco  34238  1cvratex  34239  1cvrjat  34241  polval2N  34672  polsubN  34673  2polpmapN  34679  2polvalN  34680  poldmj1N  34694  pmapj2N  34695  polatN  34697  2polatN  34698  pnonsingN  34699  ispsubcl2N  34713  polsubclN  34718  poml4N  34719  pmapojoinN  34734  pl42lem1N  34745  lhpoc2N  34781  lhpocnle  34782  lhpmod2i2  34804  lhpmod6i1  34805  lhprelat3N  34806  trlcl  34931  trlle  34951  docaclN  35893  doca2N  35895  djajN  35906  dih1  36055  dih1dimatlem  36098  dochcl  36122  dochvalr3  36132  doch2val2  36133  dochss  36134  dochocss  36135  dochoc  36136  dochnoncon  36160  djhlj  36170