omnimkv - Intuitionistic Logic Explorer

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

Theorem omnimkv 7284

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 7264	. . . 4 Omni Omni $\/$
2	1	ibi 176	. . 3 Omni $\/$
3		pm2.53 724	. . . . . . 7 $\/$
4	3	orcoms 732	. . . . . 6 $\/$
5	4	a1i 9	. . . . 5 Omni $\/$
6	5	imim2d 54	. . . 4 Omni $\/$
7	6	alimdv 1903	. . 3 Omni $\/$
8	2, 7	mpd 13	. 2 Omni
9		ismkv 7281	. 2 Omni Markov
10	8, 9	mpbird 167	1 Omni Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 710

wal 1371

wceq 1373

wcel 2178

wral 2486

wrex 2487

c0 3468

wf 5286

cfv 5290

c1o 6518

c2o 6519 Omnicomni 7262 Markovcmarkov 7279

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 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-ext 2189

This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1485 df-sb 1787 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ral 2491 df-rex 2492 df-v 2778 df-fn 5293 df-f 5294 df-omni 7263 df-markov 7280

This theorem is referenced by: exmidmp 7285