omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7089

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 2720	. 2 Omni
2		simpl 108	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2722	. 2 WOmni $/\$ Markov
4		1n0 6369	. . . . . . . . . . . . . . 15
5	4	nesymi 2370	. . . . . . . . . . . . . 14
6		eqeq1 2161	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 665	. . . . . . . . . . . . 13
8	7	reximi 2551	. . . . . . . . . . . 12
9		rexnalim 2443	. . . . . . . . . . . 12
10	8, 9	syl 14	. . . . . . . . . . 11
11	10	orim1i 750	. . . . . . . . . 10 $\/$ $\/$
12	11	orcomd 719	. . . . . . . . 9 $\/$ $\/$
13		df-dc 821	. . . . . . . . 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 1801	. . 3 $\/$ DECID $/\$
29		isomni 7058	. . 3 Omni $\/$
30		iswomni 7087	. . . . . 6 WOmni DECID
31		ismkv 7075	. . . . . 6 Markov
32	30, 31	anbi12d 465	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1458	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 197	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 593	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1447	. . . 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 820

wal 1330

wceq 1332

wcel 2125

wral 2432

wrex 2433

cvv 2709

c0 3390

wf 5159

cfv 5163

c1o 6346

c2o 6347 Omnicomni 7056 Markovcmarkov 7073 WOmnicwomni 7085

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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-ext 2136 ax-nul 4086

This theorem depends on definitions: df-bi 116 df-dc 821 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-ral 2437 df-rex 2438 df-v 2711 df-dif 3100 df-un 3102 df-nul 3391 df-sn 3562 df-suc 4326 df-fn 5166 df-f 5167 df-1o 6353 df-omni 7057 df-markov 7074 df-womni 7086

This theorem is referenced by: lpowlpo 7090

W3C validator