ILE Home 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