| Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > opococ | Structured version Visualization version GIF version | ||
| Description: Double negative law for orthoposets. (ococ 31376 analog.) (Contributed by NM, 13-Sep-2011.) |
| Ref | Expression |
|---|---|
| opoccl.b | ⊢ 𝐵 = (Base‘𝐾) |
| opoccl.o | ⊢ ⊥ = (oc‘𝐾) |
| Ref | Expression |
|---|---|
| opococ | ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) |
| 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 39200 | . . . 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 | simp2d 1143 | 1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2110 class class class wbr 5089 ‘cfv 6477 (class class class)co 7341 Basecbs 17112 lecple 17160 occoc 17161 joincjn 18209 meetcmee 18210 0.cp0 18319 1.cp1 18320 OPcops 39190 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-ext 2702 ax-nul 5242 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2722 df-clel 2804 df-ne 2927 df-ral 3046 df-rab 3394 df-v 3436 df-dif 3903 df-un 3905 df-ss 3917 df-nul 4282 df-if 4474 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-br 5090 df-dm 5624 df-iota 6433 df-fv 6485 df-ov 7344 df-oposet 39194 |
| This theorem is referenced by: opcon3b 39214 opcon2b 39215 oplecon3b 39218 oplecon1b 39219 opltcon1b 39223 opltcon2b 39224 oldmm2 39236 oldmm3N 39237 oldmm4 39238 oldmj1 39239 oldmj2 39240 oldmj3 39241 oldmj4 39242 olm11 39245 omllaw4 39264 cmt2N 39268 glbconN 39395 1cvratex 39491 1cvrjat 39493 polval2N 39924 2polpmapN 39931 2polvalN 39932 2polatN 39950 lhpoc2N 40033 doch2val2 41382 dochocss 41384 dochoc 41385 |
| Copyright terms: Public domain | W3C validator |