omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7178

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 2760	. 2 Omni
2		simpl 109	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2762	. 2 WOmni $/\$ Markov
4		1n0 6446	. . . . . . . . . . . . . . 15
5	4	nesymi 2403	. . . . . . . . . . . . . 14
6		eqeq1 2194	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 676	. . . . . . . . . . . . 13
8	7	reximi 2584	. . . . . . . . . . . 12
9		rexnalim 2476	. . . . . . . . . . . 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 1834	. . 3 $\/$ DECID $/\$
29		isomni 7147	. . 3 Omni $\/$
30		iswomni 7176	. . . . . 6 WOmni DECID
31		ismkv 7164	. . . . . 6 Markov
32	30, 31	anbi12d 473	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1491	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 198	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 603	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1480	. . . 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 1361

wceq 1363

wcel 2158

wral 2465

wrex 2466

cvv 2749

c0 3434

wf 5224

cfv 5228

c1o 6423

c2o 6424 Omnicomni 7145 Markovcmarkov 7162 WOmnicwomni 7174

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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 ax-nul 4141

This theorem depends on definitions: df-bi 117 df-dc 836 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-ral 2470 df-rex 2471 df-v 2751 df-dif 3143 df-un 3145 df-nul 3435 df-sn 3610 df-suc 4383 df-fn 5231 df-f 5232 df-1o 6430 df-omni 7146 df-markov 7163 df-womni 7175

This theorem is referenced by: lpowlpo 7179

W3C validator