omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7155

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 2746	. 2 Omni
2		simpl 109	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2748	. 2 WOmni $/\$ Markov
4		1n0 6423	. . . . . . . . . . . . . . 15
5	4	nesymi 2391	. . . . . . . . . . . . . 14
6		eqeq1 2182	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 675	. . . . . . . . . . . . 13
8	7	reximi 2572	. . . . . . . . . . . 12
9		rexnalim 2464	. . . . . . . . . . . 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 1822	. . 3 $\/$ DECID $/\$
29		isomni 7124	. . 3 Omni $\/$
30		iswomni 7153	. . . . . 6 WOmni DECID
31		ismkv 7141	. . . . . 6 Markov
32	30, 31	anbi12d 473	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1479	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 198	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 603	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1468	. . . 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 2146

wral 2453

wrex 2454

cvv 2735

c0 3420

wf 5204

cfv 5208

c1o 6400

c2o 6401 Omnicomni 7122 Markovcmarkov 7139 WOmnicwomni 7151

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 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-ext 2157 ax-nul 4124

This theorem depends on definitions: df-bi 117 df-dc 835 df-tru 1356 df-fal 1359 df-nf 1459 df-sb 1761 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-ne 2346 df-ral 2458 df-rex 2459 df-v 2737 df-dif 3129 df-un 3131 df-nul 3421 df-sn 3595 df-suc 4365 df-fn 5211 df-f 5212 df-1o 6407 df-omni 7123 df-markov 7140 df-womni 7152

This theorem is referenced by: lpowlpo 7156

W3C validator