omniwomnimkv - Intuitionistic Logic Explorer

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

Theorem omniwomnimkv 7497

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 2833	. 2 Omni
2		simpl 109	. . 3 WOmni $/\$ Markov WOmni
3	2	elexd 2835	. 2 WOmni $/\$ Markov
4		1n0 6695	. . . . . . . . . . . . . . 15
5	4	nesymi 2466	. . . . . . . . . . . . . 14
6		eqeq1 2245	. . . . . . . . . . . . . 14
7	5, 6	mtbiri 686	. . . . . . . . . . . . 13
8	7	reximi 2647	. . . . . . . . . . . 12
9		rexnalim 2539	. . . . . . . . . . . 12
10	8, 9	syl 14	. . . . . . . . . . 11
11	10	orim1i 772	. . . . . . . . . 10 $\/$ $\/$
12	11	orcomd 741	. . . . . . . . 9 $\/$ $\/$
13		df-dc 847	. . . . . . . . 9 DECID $\/$
14	12, 13	sylibr 134	. . . . . . . 8 $\/$ DECID
15	14	adantl 277	. . . . . . 7 $/\$ $/\$ $\/$ DECID
16		simpr 110	. . . . . . . . 9 $/\$ $/\$ $\/$ $\/$
17	16	orcomd 741	. . . . . . . 8 $/\$ $/\$ $\/$ $\/$
18	17	ord 736	. . . . . . 7 $/\$ $/\$ $\/$
19	15, 18	jca 306	. . . . . 6 $/\$ $/\$ $\/$ DECID $/\$
20		simprl 535	. . . . . . . . 9 $/\$ $/\$ DECID $/\$ DECID
21	20, 13	sylib 122	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$
22		simprr 537	. . . . . . . . 9 $/\$ $/\$ DECID $/\$
23	22	orim2d 800	. . . . . . . 8 $/\$ $/\$ DECID $/\$ $\/$ $\/$
24	21, 23	mpd 13	. . . . . . 7 $/\$ $/\$ DECID $/\$ $\/$
25	24	orcomd 741	. . . . . 6 $/\$ $/\$ DECID $/\$ $\/$
26	19, 25	impbida 604	. . . . 5 $/\$ $\/$ DECID $/\$
27	26	pm5.74da 447	. . . 4 $\/$ DECID $/\$
28	27	albidv 1877	. . 3 $\/$ DECID $/\$
29		isomni 7466	. . 3 Omni $\/$
30		iswomni 7495	. . . . . 6 WOmni DECID
31		ismkv 7483	. . . . . 6 Markov
32	30, 31	anbi12d 477	. . . . 5 WOmni $/\$ Markov DECID $/\$
33		19.26 1534	. . . . 5 DECID $/\$ DECID $/\$
34	32, 33	bitr4di 198	. . . 4 WOmni $/\$ Markov DECID $/\$
35		jcab 611	. . . . 5 DECID $/\$ DECID $/\$
36	35	albii 1523	. . . 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 716	1 Omni WOmni $/\$ Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 720 DECID wdc 846

wal 1400

wceq 1402

wcel 2209

wral 2528

wrex 2529

cvv 2821

c0 3520

wf 5368

cfv 5372

c1o 6670

c2o 6671 Omnicomni 7464 Markovcmarkov 7481 WOmnicwomni 7493

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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-ext 2220 ax-nul 4254

This theorem depends on definitions: df-bi 117 df-dc 847 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-ral 2533 df-rex 2534 df-v 2823 df-dif 3222 df-un 3224 df-nul 3521 df-sn 3711 df-suc 4511 df-fn 5375 df-f 5376 df-1o 6677 df-omni 7465 df-markov 7482 df-womni 7494

This theorem is referenced by: lpowlpo 7498

W3C validator