omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7131

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 2737	. 2 Omni
2		simpl 108	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2739	. 2 WOmni $/\$ Markov
4		1n0 6400	. . . . . . . . . . . . . . 15
5	4	nesymi 2382	. . . . . . . . . . . . . 14
6		eqeq1 2172	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 665	. . . . . . . . . . . . 13
8	7	reximi 2563	. . . . . . . . . . . 12
9		rexnalim 2455	. . . . . . . . . . . 12
10	8, 9	syl 14	. . . . . . . . . . 11
11	10	orim1i 750	. . . . . . . . . 10 $\/$ $\/$
12	11	orcomd 719	. . . . . . . . 9 $\/$ $\/$
13		df-dc 825	. . . . . . . . 9 DECID $\/$
14	12, 13	sylibr 133	. . . . . . . 8 $\/$ DECID
15	14	adantl 275	. . . . . . 7 $/\$ $/\$ $\/$ DECID
16		simpr 109	. . . . . . . . 9 $/\$ $/\$ $\/$ $\/$
17	16	orcomd 719	. . . . . . . 8 $/\$ $/\$ $\/$ $\/$
18	17	ord 714	. . . . . . 7 $/\$ $/\$ $\/$
19	15, 18	jca 304	. . . . . 6 $/\$ $/\$ $\/$ DECID $/\$
20		simprl 521	. . . . . . . . 9 $/\$ $/\$ DECID $/\$ DECID
21	20, 13	sylib 121	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$
22		simprr 522	. . . . . . . . 9 $/\$ $/\$ DECID $/\$
23	22	orim2d 778	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$ $\/$
24	21, 23	mpd 13	. . . . . . 7 $/\$ $/\$ DECID $/\$ $\/$
25	24	orcomd 719	. . . . . 6 $/\$ $/\$ DECID $/\$ $\/$
26	19, 25	impbida 586	. . . . 5 $/\$ $\/$ DECID $/\$
27	26	pm5.74da 440	. . . 4 $\/$ DECID $/\$
28	27	albidv 1812	. . 3 $\/$ DECID $/\$
29		isomni 7100	. . 3 Omni $\/$
30		iswomni 7129	. . . . . 6 WOmni DECID
31		ismkv 7117	. . . . . 6 Markov
32	30, 31	anbi12d 465	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1469	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 197	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 593	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1458	. . . 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 694	1 Omni WOmni $/\$ Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698 DECID wdc 824

wal 1341

wceq 1343

wcel 2136

wral 2444

wrex 2445

cvv 2726

c0 3409

wf 5184

cfv 5188

c1o 6377

c2o 6378 Omnicomni 7098 Markovcmarkov 7115 WOmnicwomni 7127

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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-ext 2147 ax-nul 4108

This theorem depends on definitions: df-bi 116 df-dc 825 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-v 2728 df-dif 3118 df-un 3120 df-nul 3410 df-sn 3582 df-suc 4349 df-fn 5191 df-f 5192 df-1o 6384 df-omni 7099 df-markov 7116 df-womni 7128

This theorem is referenced by: lpowlpo 7132

W3C validator