omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7365

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 2814	. 2 Omni
2		simpl 109	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2816	. 2 WOmni $/\$ Markov
4		1n0 6599	. . . . . . . . . . . . . . 15
5	4	nesymi 2448	. . . . . . . . . . . . . 14
6		eqeq1 2238	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 681	. . . . . . . . . . . . 13
8	7	reximi 2629	. . . . . . . . . . . 12
9		rexnalim 2521	. . . . . . . . . . . 12
10	8, 9	syl 14	. . . . . . . . . . 11
11	10	orim1i 767	. . . . . . . . . 10 $\/$ $\/$
12	11	orcomd 736	. . . . . . . . 9 $\/$ $\/$
13		df-dc 842	. . . . . . . . 9 DECID $\/$
14	12, 13	sylibr 134	. . . . . . . 8 $\/$ DECID
15	14	adantl 277	. . . . . . 7 $/\$ $/\$ $\/$ DECID
16		simpr 110	. . . . . . . . 9 $/\$ $/\$ $\/$ $\/$
17	16	orcomd 736	. . . . . . . 8 $/\$ $/\$ $\/$ $\/$
18	17	ord 731	. . . . . . 7 $/\$ $/\$ $\/$
19	15, 18	jca 306	. . . . . 6 $/\$ $/\$ $\/$ DECID $/\$
20		simprl 531	. . . . . . . . 9 $/\$ $/\$ DECID $/\$ DECID
21	20, 13	sylib 122	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$
22		simprr 533	. . . . . . . . 9 $/\$ $/\$ DECID $/\$
23	22	orim2d 795	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$ $\/$
24	21, 23	mpd 13	. . . . . . 7 $/\$ $/\$ DECID $/\$ $\/$
25	24	orcomd 736	. . . . . 6 $/\$ $/\$ DECID $/\$ $\/$
26	19, 25	impbida 600	. . . . 5 $/\$ $\/$ DECID $/\$
27	26	pm5.74da 443	. . . 4 $\/$ DECID $/\$
28	27	albidv 1872	. . 3 $\/$ DECID $/\$
29		isomni 7334	. . 3 Omni $\/$
30		iswomni 7363	. . . . . 6 WOmni DECID
31		ismkv 7351	. . . . . 6 Markov
32	30, 31	anbi12d 473	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1529	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 198	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 607	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1518	. . . 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 711	1 Omni WOmni $/\$ Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 715 DECID wdc 841

wal 1395

wceq 1397

wcel 2202

wral 2510

wrex 2511

cvv 2802

c0 3494

wf 5322

cfv 5326

c1o 6574

c2o 6575 Omnicomni 7332 Markovcmarkov 7349 WOmnicwomni 7361

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-ext 2213 ax-nul 4215

This theorem depends on definitions: df-bi 117 df-dc 842 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-ral 2515 df-rex 2516 df-v 2804 df-dif 3202 df-un 3204 df-nul 3495 df-sn 3675 df-suc 4468 df-fn 5329 df-f 5330 df-1o 6581 df-omni 7333 df-markov 7350 df-womni 7362

This theorem is referenced by: lpowlpo 7366

W3C validator