![]() |
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 31435 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 2735 | . . . . 5 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | opoccl.o | . . . . 5 ⊢ ⊥ = (oc‘𝐾) | |
4 | eqid 2735 | . . . . 5 ⊢ (join‘𝐾) = (join‘𝐾) | |
5 | eqid 2735 | . . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
6 | eqid 2735 | . . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
7 | eqid 2735 | . . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 39164 | . . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
9 | 8 | 3anidm23 1420 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
10 | 9 | simp1d 1141 | . 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋)))) |
11 | 10 | simp2d 1142 | 1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 class class class wbr 5148 ‘cfv 6563 (class class class)co 7431 Basecbs 17245 lecple 17305 occoc 17306 joincjn 18369 meetcmee 18370 0.cp0 18481 1.cp1 18482 OPcops 39154 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-nul 5312 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ne 2939 df-ral 3060 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-br 5149 df-dm 5699 df-iota 6516 df-fv 6571 df-ov 7434 df-oposet 39158 |
This theorem is referenced by: opcon3b 39178 opcon2b 39179 oplecon3b 39182 oplecon1b 39183 opltcon1b 39187 opltcon2b 39188 oldmm2 39200 oldmm3N 39201 oldmm4 39202 oldmj1 39203 oldmj2 39204 oldmj3 39205 oldmj4 39206 olm11 39209 omllaw4 39228 cmt2N 39232 glbconN 39359 glbconNOLD 39360 1cvratex 39456 1cvrjat 39458 polval2N 39889 2polpmapN 39896 2polvalN 39897 2polatN 39915 lhpoc2N 39998 doch2val2 41347 dochocss 41349 dochoc 41350 |
Copyright terms: Public domain | W3C validator |