omnimkv - Intuitionistic Logic Explorer

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

Theorem omnimkv 7319

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 7299	. . . 4 Omni Omni $\/$
2	1	ibi 176	. . 3 Omni $\/$
3		pm2.53 727	. . . . . . 7 $\/$
4	3	orcoms 735	. . . . . 6 $\/$
5	4	a1i 9	. . . . 5 Omni $\/$
6	5	imim2d 54	. . . 4 Omni $\/$
7	6	alimdv 1925	. . 3 Omni $\/$
8	2, 7	mpd 13	. 2 Omni
9		ismkv 7316	. 2 Omni Markov
10	8, 9	mpbird 167	1 Omni Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 713

wal 1393

wceq 1395

wcel 2200

wral 2508

wrex 2509

c0 3491

wf 5313

cfv 5317

c1o 6553

c2o 6554 Omnicomni 7297 Markovcmarkov 7314

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-ext 2211

This theorem depends on definitions: df-bi 117 df-tru 1398 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-v 2801 df-fn 5320 df-f 5321 df-omni 7298 df-markov 7315

This theorem is referenced by: exmidmp 7320