![]() |
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 30924 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 38357 | . . . 4 β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β ((( β₯ βπ) β π΅ β§ ( β₯ β( β₯ βπ)) = π β§ (π(leβπΎ)π β ( β₯ βπ)(leβπΎ)( β₯ βπ))) β§ (π(joinβπΎ)( β₯ βπ)) = (1.βπΎ) β§ (π(meetβπΎ)( β₯ βπ)) = (0.βπΎ))) |
9 | 8 | 3anidm23 1419 | . . 3 β’ ((πΎ β OP β§ π β π΅) β ((( β₯ βπ) β π΅ β§ ( β₯ β( β₯ βπ)) = π β§ (π(leβπΎ)π β ( β₯ βπ)(leβπΎ)( β₯ βπ))) β§ (π(joinβπΎ)( β₯ βπ)) = (1.βπΎ) β§ (π(meetβπΎ)( β₯ βπ)) = (0.βπΎ))) |
10 | 9 | simp1d 1140 | . 2 β’ ((πΎ β OP β§ π β π΅) β (( β₯ βπ) β π΅ β§ ( β₯ β( β₯ βπ)) = π β§ (π(leβπΎ)π β ( β₯ βπ)(leβπΎ)( β₯ βπ)))) |
11 | 10 | simp2d 1141 | 1 β’ ((πΎ β OP β§ π β π΅) β ( β₯ β( β₯ βπ)) = π) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 394 β§ w3a 1085 = wceq 1539 β wcel 2104 class class class wbr 5149 βcfv 6544 (class class class)co 7413 Basecbs 17150 lecple 17210 occoc 17211 joincjn 18270 meetcmee 18271 0.cp0 18382 1.cp1 18383 OPcops 38347 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 ax-nul 5307 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ne 2939 df-ral 3060 df-rab 3431 df-v 3474 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-dm 5687 df-iota 6496 df-fv 6552 df-ov 7416 df-oposet 38351 |
This theorem is referenced by: opcon3b 38371 opcon2b 38372 oplecon3b 38375 oplecon1b 38376 opltcon1b 38380 opltcon2b 38381 oldmm2 38393 oldmm3N 38394 oldmm4 38395 oldmj1 38396 oldmj2 38397 oldmj3 38398 oldmj4 38399 olm11 38402 omllaw4 38421 cmt2N 38425 glbconN 38552 glbconNOLD 38553 1cvratex 38649 1cvrjat 38651 polval2N 39082 2polpmapN 39089 2polvalN 39090 2polatN 39108 lhpoc2N 39191 doch2val2 40540 dochocss 40542 dochoc 40543 |
Copyright terms: Public domain | W3C validator |