omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7159

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 2748	. 2 Omni
2		simpl 109	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2750	. 2 WOmni $/\$ Markov
4		1n0 6427	. . . . . . . . . . . . . . 15
5	4	nesymi 2393	. . . . . . . . . . . . . 14
6		eqeq1 2184	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 675	. . . . . . . . . . . . 13
8	7	reximi 2574	. . . . . . . . . . . 12
9		rexnalim 2466	. . . . . . . . . . . 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 1824	. . 3 $\/$ DECID $/\$
29		isomni 7128	. . 3 Omni $\/$
30		iswomni 7157	. . . . . 6 WOmni DECID
31		ismkv 7145	. . . . . 6 Markov
32	30, 31	anbi12d 473	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1481	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 198	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 603	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1470	. . . 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 2148

wral 2455

wrex 2456

cvv 2737

c0 3422

wf 5208

cfv 5212

c1o 6404

c2o 6405 Omnicomni 7126 Markovcmarkov 7143 WOmnicwomni 7155

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 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-nul 4126

This theorem depends on definitions: df-bi 117 df-dc 835 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-v 2739 df-dif 3131 df-un 3133 df-nul 3423 df-sn 3597 df-suc 4368 df-fn 5215 df-f 5216 df-1o 6411 df-omni 7127 df-markov 7144 df-womni 7156

This theorem is referenced by: lpowlpo 7160

W3C validator