omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7143

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 2741	. 2 Omni
2		simpl 108	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2743	. 2 WOmni $/\$ Markov
4		1n0 6411	. . . . . . . . . . . . . . 15
5	4	nesymi 2386	. . . . . . . . . . . . . 14
6		eqeq1 2177	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 670	. . . . . . . . . . . . 13
8	7	reximi 2567	. . . . . . . . . . . 12
9		rexnalim 2459	. . . . . . . . . . . 12
10	8, 9	syl 14	. . . . . . . . . . 11
11	10	orim1i 755	. . . . . . . . . 10 $\/$ $\/$
12	11	orcomd 724	. . . . . . . . 9 $\/$ $\/$
13		df-dc 830	. . . . . . . . 9 DECID $\/$
14	12, 13	sylibr 133	. . . . . . . 8 $\/$ DECID
15	14	adantl 275	. . . . . . 7 $/\$ $/\$ $\/$ DECID
16		simpr 109	. . . . . . . . 9 $/\$ $/\$ $\/$ $\/$
17	16	orcomd 724	. . . . . . . 8 $/\$ $/\$ $\/$ $\/$
18	17	ord 719	. . . . . . 7 $/\$ $/\$ $\/$
19	15, 18	jca 304	. . . . . 6 $/\$ $/\$ $\/$ DECID $/\$
20		simprl 526	. . . . . . . . 9 $/\$ $/\$ DECID $/\$ DECID
21	20, 13	sylib 121	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$
22		simprr 527	. . . . . . . . 9 $/\$ $/\$ DECID $/\$
23	22	orim2d 783	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$ $\/$
24	21, 23	mpd 13	. . . . . . 7 $/\$ $/\$ DECID $/\$ $\/$
25	24	orcomd 724	. . . . . 6 $/\$ $/\$ DECID $/\$ $\/$
26	19, 25	impbida 591	. . . . 5 $/\$ $\/$ DECID $/\$
27	26	pm5.74da 441	. . . 4 $\/$ DECID $/\$
28	27	albidv 1817	. . 3 $\/$ DECID $/\$
29		isomni 7112	. . 3 Omni $\/$
30		iswomni 7141	. . . . . 6 WOmni DECID
31		ismkv 7129	. . . . . 6 Markov
32	30, 31	anbi12d 470	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1474	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 197	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 598	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1463	. . . 4 DECID $/\$ DECID $/\$
37	34, 36	bitr4di 197	. . 3 WOmni $/\$ Markov DECID $/\$
38	28, 29, 37	3bitr4d 219	. 2 Omni WOmni $/\$ Markov
39	1, 3, 38	pm5.21nii 699	1 Omni WOmni $/\$ Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 703 DECID wdc 829

wal 1346

wceq 1348

wcel 2141

wral 2448

wrex 2449

cvv 2730

c0 3414

wf 5194

cfv 5198

c1o 6388

c2o 6389 Omnicomni 7110 Markovcmarkov 7127 WOmnicwomni 7139

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-nul 4115

This theorem depends on definitions: df-bi 116 df-dc 830 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-ral 2453 df-rex 2454 df-v 2732 df-dif 3123 df-un 3125 df-nul 3415 df-sn 3589 df-suc 4356 df-fn 5201 df-f 5202 df-1o 6395 df-omni 7111 df-markov 7128 df-womni 7140

This theorem is referenced by: lpowlpo 7144

W3C validator