| 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 31425 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 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.‘𝐾) | |
| 8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 39183 | . . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
| 9 | 8 | 3anidm23 1423 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
| 10 | 9 | simp1d 1143 | . 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋)))) |
| 11 | 10 | simp2d 1144 | 1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 class class class wbr 5143 ‘cfv 6561 (class class class)co 7431 Basecbs 17247 lecple 17304 occoc 17305 joincjn 18357 meetcmee 18358 0.cp0 18468 1.cp1 18469 OPcops 39173 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-nul 5306 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-dm 5695 df-iota 6514 df-fv 6569 df-ov 7434 df-oposet 39177 |
| This theorem is referenced by: opcon3b 39197 opcon2b 39198 oplecon3b 39201 oplecon1b 39202 opltcon1b 39206 opltcon2b 39207 oldmm2 39219 oldmm3N 39220 oldmm4 39221 oldmj1 39222 oldmj2 39223 oldmj3 39224 oldmj4 39225 olm11 39228 omllaw4 39247 cmt2N 39251 glbconN 39378 glbconNOLD 39379 1cvratex 39475 1cvrjat 39477 polval2N 39908 2polpmapN 39915 2polvalN 39916 2polatN 39934 lhpoc2N 40017 doch2val2 41366 dochocss 41368 dochoc 41369 |
| Copyright terms: Public domain | W3C validator |