omnimkv - Intuitionistic Logic Explorer

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

Theorem omnimkv 6980

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 6958	. . . 4 Omni Omni $\/$
2	1	ibi 175	. . 3 Omni $\/$
3		pm2.53 694	. . . . . . 7 $\/$
4	3	orcoms 702	. . . . . 6 $\/$
5	4	a1i 9	. . . . 5 Omni $\/$
6	5	imim2d 54	. . . 4 Omni $\/$
7	6	alimdv 1833	. . 3 Omni $\/$
8	2, 7	mpd 13	. 2 Omni
9		ismkv 6977	. 2 Omni Markov
10	8, 9	mpbird 166	1 Omni Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 680

wal 1312

wceq 1314

wcel 1463

wral 2390

wrex 2391

c0 3329

wf 5077

cfv 5081

c1o 6260

c2o 6261 Omnicomni 6954 Markovcmarkov 6975

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097

This theorem depends on definitions: df-bi 116 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-v 2659 df-fn 5084 df-f 5085 df-omni 6956 df-markov 6976

This theorem is referenced by: exmidmp 6981