Theorem omnimkv 7172

Description: An omniscient set is Markov. In particular, the case where 𝐴 is ω 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 7152	. . . 4 ⊢ (𝐴 ∈ Omni → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))))
2	1	ibi 176	. . 3 ⊢ (𝐴 ∈ Omni → ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))
3		pm2.53 723	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))
4	3	orcoms 731	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))
5	4	a1i 9	. . . . 5 ⊢ (𝐴 ∈ Omni → ((∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))
6	5	imim2d 54	. . . 4 ⊢ (𝐴 ∈ Omni → ((𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) → (𝑓:𝐴⟶2o → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))
7	6	alimdv 1890	. . 3 ⊢ (𝐴 ∈ Omni → (∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) → ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))
8	2, 7	mpd 13	. 2 ⊢ (𝐴 ∈ Omni → ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))
9		ismkv 7169	. 2 ⊢ (𝐴 ∈ Omni → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))
10	8, 9	mpbird 167	1 ⊢ (𝐴 ∈ Omni → 𝐴 ∈ Markov)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 709  ∀wal 1362   = wceq 1364   ∈ wcel 2160  ∀wral 2468  ∃wrex 2469  ∅c0 3437  ⟶wf 5227  ‘cfv 5231  1_oc1o 6428  2_oc2o 6429  Omnicomni 7150  Markovcmarkov 7167

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-fn 5234  df-f 5235  df-omni 7151  df-markov 7168

This theorem is referenced by:  exmidmp  7173