Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > omniwomnimkv | Unicode version |
Description: A set is omniscient if and only if it is weakly omniscient and Markov. The case says that LPO WLPO MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.) |
Ref | Expression |
---|---|
omniwomnimkv | Omni WOmni Markov |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2746 | . 2 Omni | |
2 | simpl 109 | . . 3 WOmni Markov WOmni | |
3 | 2 | elexd 2748 | . 2 WOmni Markov |
4 | 1n0 6423 | . . . . . . . . . . . . . . 15 | |
5 | 4 | nesymi 2391 | . . . . . . . . . . . . . 14 |
6 | eqeq1 2182 | . . . . . . . . . . . . . 14 | |
7 | 5, 6 | mtbiri 675 | . . . . . . . . . . . . 13 |
8 | 7 | reximi 2572 | . . . . . . . . . . . 12 |
9 | rexnalim 2464 | . . . . . . . . . . . 12 | |
10 | 8, 9 | syl 14 | . . . . . . . . . . 11 |
11 | 10 | orim1i 760 | . . . . . . . . . 10 |
12 | 11 | orcomd 729 | . . . . . . . . 9 |
13 | df-dc 835 | . . . . . . . . 9 DECID | |
14 | 12, 13 | sylibr 134 | . . . . . . . 8 DECID |
15 | 14 | adantl 277 | . . . . . . 7 DECID |
16 | simpr 110 | . . . . . . . . 9 | |
17 | 16 | orcomd 729 | . . . . . . . 8 |
18 | 17 | ord 724 | . . . . . . 7 |
19 | 15, 18 | jca 306 | . . . . . 6 DECID |
20 | simprl 529 | . . . . . . . . 9 DECID DECID | |
21 | 20, 13 | sylib 122 | . . . . . . . 8 DECID |
22 | simprr 531 | . . . . . . . . 9 DECID | |
23 | 22 | orim2d 788 | . . . . . . . 8 DECID |
24 | 21, 23 | mpd 13 | . . . . . . 7 DECID |
25 | 24 | orcomd 729 | . . . . . 6 DECID |
26 | 19, 25 | impbida 596 | . . . . 5 DECID |
27 | 26 | pm5.74da 443 | . . . 4 DECID |
28 | 27 | albidv 1822 | . . 3 DECID |
29 | isomni 7124 | . . 3 Omni | |
30 | iswomni 7153 | . . . . . 6 WOmni DECID | |
31 | ismkv 7141 | . . . . . 6 Markov | |
32 | 30, 31 | anbi12d 473 | . . . . 5 WOmni Markov DECID |
33 | 19.26 1479 | . . . . 5 DECID DECID | |
34 | 32, 33 | bitr4di 198 | . . . 4 WOmni Markov DECID |
35 | jcab 603 | . . . . 5 DECID DECID | |
36 | 35 | albii 1468 | . . . 4 DECID DECID |
37 | 34, 36 | bitr4di 198 | . . 3 WOmni Markov DECID |
38 | 28, 29, 37 | 3bitr4d 220 | . 2 Omni WOmni Markov |
39 | 1, 3, 38 | pm5.21nii 704 | 1 Omni WOmni Markov |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 104 wb 105 wo 708 DECID wdc 834 wal 1351 wceq 1353 wcel 2146 wral 2453 wrex 2454 cvv 2735 c0 3420 wf 5204 cfv 5208 c1o 6400 c2o 6401 Omnicomni 7122 Markovcmarkov 7139 WOmnicwomni 7151 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-ext 2157 ax-nul 4124 |
This theorem depends on definitions: df-bi 117 df-dc 835 df-tru 1356 df-fal 1359 df-nf 1459 df-sb 1761 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-ne 2346 df-ral 2458 df-rex 2459 df-v 2737 df-dif 3129 df-un 3131 df-nul 3421 df-sn 3595 df-suc 4365 df-fn 5211 df-f 5212 df-1o 6407 df-omni 7123 df-markov 7140 df-womni 7152 |
This theorem is referenced by: lpowlpo 7156 |
Copyright terms: Public domain | W3C validator |