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

Theorem mkvprop 7039
 Description: Markov's Principle expressed in terms of propositions (or more precisely, the 𝐴 = ω case is Markov's Principle). (Contributed by Jim Kingdon, 19-Mar-2023.)
Assertion
Ref Expression
mkvprop ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → ∃𝑛𝐴 𝜑)
Distinct variable group:   𝐴,𝑛
Allowed substitution hint:   𝜑(𝑛)

Proof of Theorem mkvprop
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 nfv 1509 . . . . . . 7 𝑛 𝐴 ∈ Markov
2 nfra1 2469 . . . . . . 7 𝑛𝑛𝐴 DECID 𝜑
31, 2nfan 1545 . . . . . 6 𝑛(𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑)
4 simpr 109 . . . . . . . . 9 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑) ∧ 𝑛𝐴) → 𝑛𝐴)
5 0lt2o 6345 . . . . . . . . . . . 12 ∅ ∈ 2o
65a1i 9 . . . . . . . . . . 11 ((∀𝑛𝐴 DECID 𝜑𝑛𝐴) → ∅ ∈ 2o)
7 1lt2o 6346 . . . . . . . . . . . 12 1o ∈ 2o
87a1i 9 . . . . . . . . . . 11 ((∀𝑛𝐴 DECID 𝜑𝑛𝐴) → 1o ∈ 2o)
9 rsp 2483 . . . . . . . . . . . 12 (∀𝑛𝐴 DECID 𝜑 → (𝑛𝐴DECID 𝜑))
109imp 123 . . . . . . . . . . 11 ((∀𝑛𝐴 DECID 𝜑𝑛𝐴) → DECID 𝜑)
116, 8, 10ifcldcd 3511 . . . . . . . . . 10 ((∀𝑛𝐴 DECID 𝜑𝑛𝐴) → if(𝜑, ∅, 1o) ∈ 2o)
1211adantll 468 . . . . . . . . 9 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑) ∧ 𝑛𝐴) → if(𝜑, ∅, 1o) ∈ 2o)
13 eqid 2140 . . . . . . . . . 10 (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) = (𝑛𝐴 ↦ if(𝜑, ∅, 1o))
1413fvmpt2 5511 . . . . . . . . 9 ((𝑛𝐴 ∧ if(𝜑, ∅, 1o) ∈ 2o) → ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = if(𝜑, ∅, 1o))
154, 12, 14syl2anc 409 . . . . . . . 8 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑) ∧ 𝑛𝐴) → ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = if(𝜑, ∅, 1o))
1615eqeq1d 2149 . . . . . . 7 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑) ∧ 𝑛𝐴) → (((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o ↔ if(𝜑, ∅, 1o) = 1o))
17 1n0 6336 . . . . . . . . . 10 1o ≠ ∅
1817nesymi 2355 . . . . . . . . 9 ¬ ∅ = 1o
19 iftrue 3483 . . . . . . . . . 10 (𝜑 → if(𝜑, ∅, 1o) = ∅)
2019eqeq1d 2149 . . . . . . . . 9 (𝜑 → (if(𝜑, ∅, 1o) = 1o ↔ ∅ = 1o))
2118, 20mtbiri 665 . . . . . . . 8 (𝜑 → ¬ if(𝜑, ∅, 1o) = 1o)
2221con2i 617 . . . . . . 7 (if(𝜑, ∅, 1o) = 1o → ¬ 𝜑)
2316, 22syl6bi 162 . . . . . 6 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑) ∧ 𝑛𝐴) → (((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o → ¬ 𝜑))
243, 23ralimdaa 2501 . . . . 5 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑) → (∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o → ∀𝑛𝐴 ¬ 𝜑))
2524con3d 621 . . . 4 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑) → (¬ ∀𝑛𝐴 ¬ 𝜑 → ¬ ∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o))
26253impia 1179 . . 3 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → ¬ ∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o)
27 mptexg 5652 . . . . 5 (𝐴 ∈ Markov → (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) ∈ V)
28273ad2ant1 1003 . . . 4 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) ∈ V)
29 ismkv 7034 . . . . . 6 (𝐴 ∈ Markov → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑛𝐴 (𝑓𝑛) = 1o → ∃𝑛𝐴 (𝑓𝑛) = ∅))))
3029ibi 175 . . . . 5 (𝐴 ∈ Markov → ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑛𝐴 (𝑓𝑛) = 1o → ∃𝑛𝐴 (𝑓𝑛) = ∅)))
31303ad2ant1 1003 . . . 4 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑛𝐴 (𝑓𝑛) = 1o → ∃𝑛𝐴 (𝑓𝑛) = ∅)))
32 nfra1 2469 . . . . . . 7 𝑛𝑛𝐴 ¬ 𝜑
3332nfn 1637 . . . . . 6 𝑛 ¬ ∀𝑛𝐴 ¬ 𝜑
341, 2, 33nf3an 1546 . . . . 5 𝑛(𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑)
35113ad2antl2 1145 . . . . 5 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → if(𝜑, ∅, 1o) ∈ 2o)
3634, 35, 13fmptdf 5584 . . . 4 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → (𝑛𝐴 ↦ if(𝜑, ∅, 1o)):𝐴⟶2o)
37 feq1 5262 . . . . . 6 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → (𝑓:𝐴⟶2o ↔ (𝑛𝐴 ↦ if(𝜑, ∅, 1o)):𝐴⟶2o))
38 nfmpt1 4028 . . . . . . . . . 10 𝑛(𝑛𝐴 ↦ if(𝜑, ∅, 1o))
3938nfeq2 2294 . . . . . . . . 9 𝑛 𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o))
40 fveq1 5427 . . . . . . . . . 10 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → (𝑓𝑛) = ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛))
4140eqeq1d 2149 . . . . . . . . 9 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → ((𝑓𝑛) = 1o ↔ ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o))
4239, 41ralbid 2436 . . . . . . . 8 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → (∀𝑛𝐴 (𝑓𝑛) = 1o ↔ ∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o))
4342notbid 657 . . . . . . 7 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → (¬ ∀𝑛𝐴 (𝑓𝑛) = 1o ↔ ¬ ∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o))
4440eqeq1d 2149 . . . . . . . 8 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → ((𝑓𝑛) = ∅ ↔ ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅))
4539, 44rexbid 2437 . . . . . . 7 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → (∃𝑛𝐴 (𝑓𝑛) = ∅ ↔ ∃𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅))
4643, 45imbi12d 233 . . . . . 6 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → ((¬ ∀𝑛𝐴 (𝑓𝑛) = 1o → ∃𝑛𝐴 (𝑓𝑛) = ∅) ↔ (¬ ∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o → ∃𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅)))
4737, 46imbi12d 233 . . . . 5 (𝑓 = (𝑛𝐴 ↦ if(𝜑, ∅, 1o)) → ((𝑓:𝐴⟶2o → (¬ ∀𝑛𝐴 (𝑓𝑛) = 1o → ∃𝑛𝐴 (𝑓𝑛) = ∅)) ↔ ((𝑛𝐴 ↦ if(𝜑, ∅, 1o)):𝐴⟶2o → (¬ ∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o → ∃𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅))))
4847spcgv 2776 . . . 4 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o)) ∈ V → (∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑛𝐴 (𝑓𝑛) = 1o → ∃𝑛𝐴 (𝑓𝑛) = ∅)) → ((𝑛𝐴 ↦ if(𝜑, ∅, 1o)):𝐴⟶2o → (¬ ∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o → ∃𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅))))
4928, 31, 36, 48syl3c 63 . . 3 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → (¬ ∀𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = 1o → ∃𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅))
5026, 49mpd 13 . 2 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → ∃𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅)
51 simpr 109 . . . . . 6 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → 𝑛𝐴)
5251, 35, 14syl2anc 409 . . . . 5 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = if(𝜑, ∅, 1o))
5352eqeq1d 2149 . . . 4 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → (((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅ ↔ if(𝜑, ∅, 1o) = ∅))
5493ad2ant2 1004 . . . . . . 7 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → (𝑛𝐴DECID 𝜑))
5554imp 123 . . . . . 6 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → DECID 𝜑)
5617neii 2311 . . . . . . . . 9 ¬ 1o = ∅
57 simpr 109 . . . . . . . . . . 11 ((((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) ∧ ¬ 𝜑) → ¬ 𝜑)
5857iffalsed 3488 . . . . . . . . . 10 ((((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) ∧ ¬ 𝜑) → if(𝜑, ∅, 1o) = 1o)
5958eqeq1d 2149 . . . . . . . . 9 ((((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) ∧ ¬ 𝜑) → (if(𝜑, ∅, 1o) = ∅ ↔ 1o = ∅))
6056, 59mtbiri 665 . . . . . . . 8 ((((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) ∧ ¬ 𝜑) → ¬ if(𝜑, ∅, 1o) = ∅)
6160ex 114 . . . . . . 7 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → (¬ 𝜑 → ¬ if(𝜑, ∅, 1o) = ∅))
6261con2d 614 . . . . . 6 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → (if(𝜑, ∅, 1o) = ∅ → ¬ ¬ 𝜑))
63 notnotrdc 829 . . . . . 6 (DECID 𝜑 → (¬ ¬ 𝜑𝜑))
6455, 62, 63sylsyld 58 . . . . 5 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → (if(𝜑, ∅, 1o) = ∅ → 𝜑))
6564, 19impbid1 141 . . . 4 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → (if(𝜑, ∅, 1o) = ∅ ↔ 𝜑))
6653, 65bitrd 187 . . 3 (((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) ∧ 𝑛𝐴) → (((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅ ↔ 𝜑))
6734, 66rexbida 2433 . 2 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → (∃𝑛𝐴 ((𝑛𝐴 ↦ if(𝜑, ∅, 1o))‘𝑛) = ∅ ↔ ∃𝑛𝐴 𝜑))
6850, 67mpbid 146 1 ((𝐴 ∈ Markov ∧ ∀𝑛𝐴 DECID 𝜑 ∧ ¬ ∀𝑛𝐴 ¬ 𝜑) → ∃𝑛𝐴 𝜑)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103  DECID wdc 820   ∧ w3a 963  ∀wal 1330   = wceq 1332   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  Vcvv 2689  ∅c0 3367  ifcif 3478   ↦ cmpt 3996  ⟶wf 5126  ‘cfv 5130  1oc1o 6313  2oc2o 6314  Markovcmarkov 7032 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-iord 4295  df-on 4297  df-suc 4300  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-1o 6320  df-2o 6321  df-markov 7033 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator