omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7167

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 2750	. 2 Omni
2		simpl 109	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2752	. 2 WOmni $/\$ Markov
4		1n0 6435	. . . . . . . . . . . . . . 15
5	4	nesymi 2393	. . . . . . . . . . . . . 14
6		eqeq1 2184	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 675	. . . . . . . . . . . . 13
8	7	reximi 2574	. . . . . . . . . . . 12
9		rexnalim 2466	. . . . . . . . . . . 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 1824	. . 3 $\/$ DECID $/\$
29		isomni 7136	. . 3 Omni $\/$
30		iswomni 7165	. . . . . 6 WOmni DECID
31		ismkv 7153	. . . . . 6 Markov
32	30, 31	anbi12d 473	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1481	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 198	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 603	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1470	. . . 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 2148

wral 2455

wrex 2456

cvv 2739

c0 3424

wf 5214

cfv 5218

c1o 6412

c2o 6413 Omnicomni 7134 Markovcmarkov 7151 WOmnicwomni 7163

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 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-nul 4131

This theorem depends on definitions: df-bi 117 df-dc 835 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-v 2741 df-dif 3133 df-un 3135 df-nul 3425 df-sn 3600 df-suc 4373 df-fn 5221 df-f 5222 df-1o 6419 df-omni 7135 df-markov 7152 df-womni 7164

This theorem is referenced by: lpowlpo 7168

W3C validator