![]() |
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 30517 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 2731 | . . . . 5 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | opoccl.o | . . . . 5 ⊢ ⊥ = (oc‘𝐾) | |
4 | eqid 2731 | . . . . 5 ⊢ (join‘𝐾) = (join‘𝐾) | |
5 | eqid 2731 | . . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
6 | eqid 2731 | . . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
7 | eqid 2731 | . . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 37841 | . . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
9 | 8 | 3anidm23 1421 | . . 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 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 class class class wbr 5138 ‘cfv 6529 (class class class)co 7390 Basecbs 17123 lecple 17183 occoc 17184 joincjn 18243 meetcmee 18244 0.cp0 18355 1.cp1 18356 OPcops 37831 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-nul 5296 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-ral 3061 df-rab 3430 df-v 3472 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4520 df-sn 4620 df-pr 4622 df-op 4626 df-uni 4899 df-br 5139 df-dm 5676 df-iota 6481 df-fv 6537 df-ov 7393 df-oposet 37835 |
This theorem is referenced by: opcon3b 37855 opcon2b 37856 oplecon3b 37859 oplecon1b 37860 opltcon1b 37864 opltcon2b 37865 oldmm2 37877 oldmm3N 37878 oldmm4 37879 oldmj1 37880 oldmj2 37881 oldmj3 37882 oldmj4 37883 olm11 37886 omllaw4 37905 cmt2N 37909 glbconN 38036 glbconNOLD 38037 1cvratex 38133 1cvrjat 38135 polval2N 38566 2polpmapN 38573 2polvalN 38574 2polatN 38592 lhpoc2N 38675 doch2val2 40024 dochocss 40026 dochoc 40027 |
Copyright terms: Public domain | W3C validator |