Theorem opoccl 39160

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   class class class wbr 5102  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  lecple 17203  occoc 17204  joincjn 18248  meetcmee 18249  0.cp0 18358  1.cp1 18359  OPcops 39138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507  df-ov 7372  df-oposet 39142

This theorem is referenced by:  opcon2b  39163  oplecon3b  39166  oplecon1b  39167  opoc1  39168  opltcon3b  39170  opltcon1b  39171  opltcon2b  39172  riotaocN  39175  oldmm1  39183  oldmm2  39184  oldmm3N  39185  oldmm4  39186  oldmj1  39187  oldmj2  39188  oldmj3  39189  oldmj4  39190  olm11  39193  latmassOLD  39195  omllaw2N  39210  omllaw4  39212  cmtcomlemN  39214  cmt2N  39216  cmt3N  39217  cmt4N  39218  cmtbr2N  39219  cmtbr3N  39220  cmtbr4N  39221  lecmtN  39222  omlfh1N  39224  omlfh3N  39225  omlspjN  39227  cvrcon3b  39243  cvrcmp2  39250  atlatmstc  39285  glbconN  39343  glbconNOLD  39344  glbconxN  39345  cvrexch  39387  1cvrco  39439  1cvratex  39440  1cvrjat  39442  polval2N  39873  polsubN  39874  2polpmapN  39880  2polvalN  39881  poldmj1N  39895  pmapj2N  39896  polatN  39898  2polatN  39899  pnonsingN  39900  ispsubcl2N  39914  polsubclN  39919  poml4N  39920  pmapojoinN  39935  pl42lem1N  39946  lhpoc2N  39982  lhpocnle  39983  lhpmod2i2  40005  lhpmod6i1  40006  lhprelat3N  40007  trlcl  40131  trlle  40151  docaclN  41091  doca2N  41093  djajN  41104  dih1  41253  dih1dimatlem  41296  dochcl  41320  dochvalr3  41330  doch2val2  41331  dochss  41332  dochocss  41333  dochoc  41334  dochnoncon  41358  djhlj  41368