omniwomnimkv - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > omniwomnimkv		Unicode version

Theorem omniwomnimkv 7242

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.)

**Assertion**
Ref	Expression
omniwomnimkv	Omni WOmni $/\$ Markov

Proof of Theorem omniwomnimkv Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2774	. 2 Omni
2		simpl 109	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2776	. 2 WOmni $/\$ Markov
4		1n0 6499	. . . . . . . . . . . . . . 15
5	4	nesymi 2413	. . . . . . . . . . . . . 14
6		eqeq1 2203	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 676	. . . . . . . . . . . . 13
8	7	reximi 2594	. . . . . . . . . . . 12
9		rexnalim 2486	. . . . . . . . . . . 12
10	8, 9	syl 14	. . . . . . . . . . 11
11	10	orim1i 761	. . . . . . . . . 10 $\/$ $\/$
12	11	orcomd 730	. . . . . . . . 9 $\/$ $\/$
13		df-dc 836	. . . . . . . . 9 DECID $\/$
14	12, 13	sylibr 134	. . . . . . . 8 $\/$ DECID
15	14	adantl 277	. . . . . . 7 $/\$ $/\$ $\/$ DECID
16		simpr 110	. . . . . . . . 9 $/\$ $/\$ $\/$ $\/$
17	16	orcomd 730	. . . . . . . 8 $/\$ $/\$ $\/$ $\/$
18	17	ord 725	. . . . . . 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 789	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$ $\/$
24	21, 23	mpd 13	. . . . . . 7 $/\$ $/\$ DECID $/\$ $\/$
25	24	orcomd 730	. . . . . 6 $/\$ $/\$ DECID $/\$ $\/$
26	19, 25	impbida 596	. . . . 5 $/\$ $\/$ DECID $/\$
27	26	pm5.74da 443	. . . 4 $\/$ DECID $/\$
28	27	albidv 1838	. . 3 $\/$ DECID $/\$
29		isomni 7211	. . 3 Omni $\/$
30		iswomni 7240	. . . . . 6 WOmni DECID
31		ismkv 7228	. . . . . 6 Markov
32	30, 31	anbi12d 473	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1495	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 198	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 603	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1484	. . . 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 705	1 Omni WOmni $/\$ Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 DECID wdc 835

wal 1362

wceq 1364

wcel 2167

wral 2475

wrex 2476

cvv 2763

c0 3451

wf 5255

cfv 5259

c1o 6476

c2o 6477 Omnicomni 7209 Markovcmarkov 7226 WOmnicwomni 7238

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-ext 2178 ax-nul 4160

This theorem depends on definitions: df-bi 117 df-dc 836 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-ral 2480 df-rex 2481 df-v 2765 df-dif 3159 df-un 3161 df-nul 3452 df-sn 3629 df-suc 4407 df-fn 5262 df-f 5263 df-1o 6483 df-omni 7210 df-markov 7227 df-womni 7239

This theorem is referenced by: lpowlpo 7243

W3C validator