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

Theorem omniwomnimkv 7048
 Description: A set is omniscient if and only if it is weakly omniscient and Markov. The case 𝐴 = ω says that LPO ↔ WLPO ∧ MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.)
Assertion
Ref Expression
omniwomnimkv (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov))

Proof of Theorem omniwomnimkv
Dummy variables 𝑓 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2700 . 2 (𝐴 ∈ Omni → 𝐴 ∈ V)
2 simpl 108 . . 3 ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) → 𝐴 ∈ WOmni)
32elexd 2702 . 2 ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) → 𝐴 ∈ V)
4 1n0 6336 . . . . . . . . . . . . . . 15 1o ≠ ∅
54nesymi 2355 . . . . . . . . . . . . . 14 ¬ ∅ = 1o
6 eqeq1 2147 . . . . . . . . . . . . . 14 ((𝑓𝑥) = ∅ → ((𝑓𝑥) = 1o ↔ ∅ = 1o))
75, 6mtbiri 665 . . . . . . . . . . . . 13 ((𝑓𝑥) = ∅ → ¬ (𝑓𝑥) = 1o)
87reximi 2532 . . . . . . . . . . . 12 (∃𝑥𝐴 (𝑓𝑥) = ∅ → ∃𝑥𝐴 ¬ (𝑓𝑥) = 1o)
9 rexnalim 2428 . . . . . . . . . . . 12 (∃𝑥𝐴 ¬ (𝑓𝑥) = 1o → ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o)
108, 9syl 14 . . . . . . . . . . 11 (∃𝑥𝐴 (𝑓𝑥) = ∅ → ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o)
1110orim1i 750 . . . . . . . . . 10 ((∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o))
1211orcomd 719 . . . . . . . . 9 ((∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o))
13 df-dc 821 . . . . . . . . 9 (DECID𝑥𝐴 (𝑓𝑥) = 1o ↔ (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o))
1412, 13sylibr 133 . . . . . . . 8 ((∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o) → DECID𝑥𝐴 (𝑓𝑥) = 1o)
1514adantl 275 . . . . . . 7 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → DECID𝑥𝐴 (𝑓𝑥) = 1o)
16 simpr 109 . . . . . . . . 9 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o))
1716orcomd 719 . . . . . . . 8 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ∃𝑥𝐴 (𝑓𝑥) = ∅))
1817ord 714 . . . . . . 7 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))
1915, 18jca 304 . . . . . 6 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))
20 simprl 521 . . . . . . . . 9 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → DECID𝑥𝐴 (𝑓𝑥) = 1o)
2120, 13sylib 121 . . . . . . . 8 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o))
22 simprr 522 . . . . . . . . 9 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))
2322orim2d 778 . . . . . . . 8 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → ((∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ∃𝑥𝐴 (𝑓𝑥) = ∅)))
2421, 23mpd 13 . . . . . . 7 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ∃𝑥𝐴 (𝑓𝑥) = ∅))
2524orcomd 719 . . . . . 6 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o))
2619, 25impbida 586 . . . . 5 ((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) → ((∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o) ↔ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
2726pm5.74da 440 . . . 4 (𝐴 ∈ V → ((𝑓:𝐴⟶2o → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) ↔ (𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
2827albidv 1797 . . 3 (𝐴 ∈ V → (∀𝑓(𝑓:𝐴⟶2o → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) ↔ ∀𝑓(𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
29 isomni 7015 . . 3 (𝐴 ∈ V → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o))))
30 iswomni 7046 . . . . . 6 (𝐴 ∈ V → (𝐴 ∈ WOmni ↔ ∀𝑓(𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o)))
31 ismkv 7034 . . . . . 6 (𝐴 ∈ V → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
3230, 31anbi12d 465 . . . . 5 (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔ (∀𝑓(𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
33 19.26 1458 . . . . 5 (∀𝑓((𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) ↔ (∀𝑓(𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
3432, 33syl6bbr 197 . . . 4 (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔ ∀𝑓((𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
35 jcab 593 . . . . 5 ((𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) ↔ ((𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
3635albii 1447 . . . 4 (∀𝑓(𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) ↔ ∀𝑓((𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
3734, 36syl6bbr 197 . . 3 (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔ ∀𝑓(𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
3828, 29, 373bitr4d 219 . 2 (𝐴 ∈ V → (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov)))
391, 3, 38pm5.21nii 694 1 (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820  ∀wal 1330   = wceq 1332   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  Vcvv 2689  ∅c0 3367  ⟶wf 5126  ‘cfv 5130  1oc1o 6313  2oc2o 6314  Omnicomni 7011  Markovcmarkov 7032  WOmnicwomni 7044 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-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-nul 4061 This theorem depends on definitions:  df-bi 116  df-dc 821  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-v 2691  df-dif 3077  df-un 3079  df-nul 3368  df-sn 3537  df-suc 4300  df-fn 5133  df-f 5134  df-1o 6320  df-omni 7013  df-markov 7033  df-womni 7045 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator