Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  opococ Structured version   Visualization version   GIF version

Theorem opococ 37660
Description: Double negative law for orthoposets. (ococ 30351 analog.) (Contributed by NM, 13-Sep-2011.)
Hypotheses
Ref Expression
opoccl.b 𝐡 = (Baseβ€˜πΎ)
opoccl.o βŠ₯ = (ocβ€˜πΎ)
Assertion
Ref Expression
opococ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋)

Proof of Theorem opococ
StepHypRef Expression
1 opoccl.b . . . . 5 𝐡 = (Baseβ€˜πΎ)
2 eqid 2737 . . . . 5 (leβ€˜πΎ) = (leβ€˜πΎ)
3 opoccl.o . . . . 5 βŠ₯ = (ocβ€˜πΎ)
4 eqid 2737 . . . . 5 (joinβ€˜πΎ) = (joinβ€˜πΎ)
5 eqid 2737 . . . . 5 (meetβ€˜πΎ) = (meetβ€˜πΎ)
6 eqid 2737 . . . . 5 (0.β€˜πΎ) = (0.β€˜πΎ)
7 eqid 2737 . . . . 5 (1.β€˜πΎ) = (1.β€˜πΎ)
81, 2, 3, 4, 5, 6, 7oposlem 37647 . . . 4 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋(leβ€˜πΎ)𝑋 β†’ ( βŠ₯ β€˜π‘‹)(leβ€˜πΎ)( βŠ₯ β€˜π‘‹))) ∧ (𝑋(joinβ€˜πΎ)( βŠ₯ β€˜π‘‹)) = (1.β€˜πΎ) ∧ (𝑋(meetβ€˜πΎ)( βŠ₯ β€˜π‘‹)) = (0.β€˜πΎ)))
983anidm23 1422 . . 3 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋(leβ€˜πΎ)𝑋 β†’ ( βŠ₯ β€˜π‘‹)(leβ€˜πΎ)( βŠ₯ β€˜π‘‹))) ∧ (𝑋(joinβ€˜πΎ)( βŠ₯ β€˜π‘‹)) = (1.β€˜πΎ) ∧ (𝑋(meetβ€˜πΎ)( βŠ₯ β€˜π‘‹)) = (0.β€˜πΎ)))
109simp1d 1143 . 2 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ (( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋(leβ€˜πΎ)𝑋 β†’ ( βŠ₯ β€˜π‘‹)(leβ€˜πΎ)( βŠ₯ β€˜π‘‹))))
1110simp2d 1144 1 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   class class class wbr 5106  β€˜cfv 6497  (class class class)co 7358  Basecbs 17084  lecple 17141  occoc 17142  joincjn 18201  meetcmee 18202  0.cp0 18313  1.cp1 18314  OPcops 37637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-nul 5264
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-dm 5644  df-iota 6449  df-fv 6505  df-ov 7361  df-oposet 37641
This theorem is referenced by:  opcon3b  37661  opcon2b  37662  oplecon3b  37665  oplecon1b  37666  opltcon1b  37670  opltcon2b  37671  oldmm2  37683  oldmm3N  37684  oldmm4  37685  oldmj1  37686  oldmj2  37687  oldmj3  37688  oldmj4  37689  olm11  37692  omllaw4  37711  cmt2N  37715  glbconN  37842  glbconNOLD  37843  1cvratex  37939  1cvrjat  37941  polval2N  38372  2polpmapN  38379  2polvalN  38380  2polatN  38398  lhpoc2N  38481  doch2val2  39830  dochocss  39832  dochoc  39833
  Copyright terms: Public domain W3C validator