omnimkv - Intuitionistic Logic Explorer

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

Theorem omnimkv 7398

Description: An omniscient set is Markov. In particular, the case where

means that the Limited Principle of Omniscience (LPO) implies Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)

**Assertion**
Ref	Expression
omnimkv	Omni Markov

Proof of Theorem omnimkv Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isomni 7378	. . . 4 Omni Omni $\/$
2	1	ibi 176	. . 3 Omni $\/$
3		pm2.53 730	. . . . . . 7 $\/$
4	3	orcoms 738	. . . . . 6 $\/$
5	4	a1i 9	. . . . 5 Omni $\/$
6	5	imim2d 54	. . . 4 Omni $\/$
7	6	alimdv 1927	. . 3 Omni $\/$
8	2, 7	mpd 13	. 2 Omni
9		ismkv 7395	. 2 Omni Markov
10	8, 9	mpbird 167	1 Omni Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 716

wal 1396

wceq 1398

wcel 2202

wral 2511

wrex 2512

c0 3496

wf 5329

cfv 5333

c1o 6618

c2o 6619 Omnicomni 7376 Markovcmarkov 7393

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-ext 2213

This theorem depends on definitions: df-bi 117 df-tru 1401 df-nf 1510 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ral 2516 df-rex 2517 df-v 2805 df-fn 5336 df-f 5337 df-omni 7377 df-markov 7394

This theorem is referenced by: exmidmp 7399