omnimkv - Intuitionistic Logic Explorer

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

Theorem omnimkv 7486

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 7466	. . . 4 Omni Omni $\/$
2	1	ibi 176	. . 3 Omni $\/$
3		pm2.53 734	. . . . . . 7 $\/$
4	3	orcoms 742	. . . . . 6 $\/$
5	4	a1i 9	. . . . 5 Omni $\/$
6	5	imim2d 54	. . . 4 Omni $\/$
7	6	alimdv 1932	. . 3 Omni $\/$
8	2, 7	mpd 13	. 2 Omni
9		ismkv 7483	. 2 Omni Markov
10	8, 9	mpbird 167	1 Omni Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 720

wal 1400

wceq 1402

wcel 2209

wral 2528

wrex 2529

c0 3520

wf 5368

cfv 5372

c1o 6670

c2o 6671 Omnicomni 7464 Markovcmarkov 7481

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

This theorem depends on definitions: df-bi 117 df-tru 1405 df-nf 1514 df-sb 1816 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ral 2533 df-rex 2534 df-v 2823 df-fn 5375 df-f 5376 df-omni 7465 df-markov 7482

This theorem is referenced by: exmidmp 7487