Theorem opoccl 38367

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   class class class wbr 5147  ‘cfv 6542  (class class class)co 7411  Basecbs 17148  lecple 17208  occoc 17209  joincjn 18268  meetcmee 18269  0.cp0 18380  1.cp1 18381  OPcops 38345

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-dm 5685  df-iota 6494  df-fv 6550  df-ov 7414  df-oposet 38349

This theorem is referenced by:  opcon2b  38370  oplecon3b  38373  oplecon1b  38374  opoc1  38375  opltcon3b  38377  opltcon1b  38378  opltcon2b  38379  riotaocN  38382  oldmm1  38390  oldmm2  38391  oldmm3N  38392  oldmm4  38393  oldmj1  38394  oldmj2  38395  oldmj3  38396  oldmj4  38397  olm11  38400  latmassOLD  38402  omllaw2N  38417  omllaw4  38419  cmtcomlemN  38421  cmt2N  38423  cmt3N  38424  cmt4N  38425  cmtbr2N  38426  cmtbr3N  38427  cmtbr4N  38428  lecmtN  38429  omlfh1N  38431  omlfh3N  38432  omlspjN  38434  cvrcon3b  38450  cvrcmp2  38457  atlatmstc  38492  glbconN  38550  glbconNOLD  38551  glbconxN  38552  cvrexch  38594  1cvrco  38646  1cvratex  38647  1cvrjat  38649  polval2N  39080  polsubN  39081  2polpmapN  39087  2polvalN  39088  poldmj1N  39102  pmapj2N  39103  polatN  39105  2polatN  39106  pnonsingN  39107  ispsubcl2N  39121  polsubclN  39126  poml4N  39127  pmapojoinN  39142  pl42lem1N  39153  lhpoc2N  39189  lhpocnle  39190  lhpmod2i2  39212  lhpmod6i1  39213  lhprelat3N  39214  trlcl  39338  trlle  39358  docaclN  40298  doca2N  40300  djajN  40311  dih1  40460  dih1dimatlem  40503  dochcl  40527  dochvalr3  40537  doch2val2  40538  dochss  40539  dochocss  40540  dochoc  40541  dochnoncon  40565  djhlj  40575