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

Theorem omniwomnimkv 7155
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 2746 . 2 (𝐴 ∈ Omni → 𝐴 ∈ V)
2 simpl 109 . . 3 ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) → 𝐴 ∈ WOmni)
32elexd 2748 . 2 ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) → 𝐴 ∈ V)
4 1n0 6423 . . . . . . . . . . . . . . 15 1o ≠ ∅
54nesymi 2391 . . . . . . . . . . . . . 14 ¬ ∅ = 1o
6 eqeq1 2182 . . . . . . . . . . . . . 14 ((𝑓𝑥) = ∅ → ((𝑓𝑥) = 1o ↔ ∅ = 1o))
75, 6mtbiri 675 . . . . . . . . . . . . 13 ((𝑓𝑥) = ∅ → ¬ (𝑓𝑥) = 1o)
87reximi 2572 . . . . . . . . . . . 12 (∃𝑥𝐴 (𝑓𝑥) = ∅ → ∃𝑥𝐴 ¬ (𝑓𝑥) = 1o)
9 rexnalim 2464 . . . . . . . . . . . 12 (∃𝑥𝐴 ¬ (𝑓𝑥) = 1o → ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o)
108, 9syl 14 . . . . . . . . . . 11 (∃𝑥𝐴 (𝑓𝑥) = ∅ → ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o)
1110orim1i 760 . . . . . . . . . 10 ((∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o))
1211orcomd 729 . . . . . . . . 9 ((∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o))
13 df-dc 835 . . . . . . . . 9 (DECID𝑥𝐴 (𝑓𝑥) = 1o ↔ (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o))
1412, 13sylibr 134 . . . . . . . 8 ((∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o) → DECID𝑥𝐴 (𝑓𝑥) = 1o)
1514adantl 277 . . . . . . 7 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → DECID𝑥𝐴 (𝑓𝑥) = 1o)
16 simpr 110 . . . . . . . . 9 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o))
1716orcomd 729 . . . . . . . 8 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ∃𝑥𝐴 (𝑓𝑥) = ∅))
1817ord 724 . . . . . . 7 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))
1915, 18jca 306 . . . . . 6 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))
20 simprl 529 . . . . . . . . 9 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → DECID𝑥𝐴 (𝑓𝑥) = 1o)
2120, 13sylib 122 . . . . . . . 8 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o))
22 simprr 531 . . . . . . . . 9 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))
2322orim2d 788 . . . . . . . 8 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → ((∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ¬ ∀𝑥𝐴 (𝑓𝑥) = 1o) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ∃𝑥𝐴 (𝑓𝑥) = ∅)))
2421, 23mpd 13 . . . . . . 7 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → (∀𝑥𝐴 (𝑓𝑥) = 1o ∨ ∃𝑥𝐴 (𝑓𝑥) = ∅))
2524orcomd 729 . . . . . 6 (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o))
2619, 25impbida 596 . . . . 5 ((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) → ((∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o) ↔ (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
2726pm5.74da 443 . . . 4 (𝐴 ∈ V → ((𝑓:𝐴⟶2o → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) ↔ (𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
2827albidv 1822 . . 3 (𝐴 ∈ V → (∀𝑓(𝑓:𝐴⟶2o → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o)) ↔ ∀𝑓(𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
29 isomni 7124 . . 3 (𝐴 ∈ V → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1o))))
30 iswomni 7153 . . . . . 6 (𝐴 ∈ V → (𝐴 ∈ WOmni ↔ ∀𝑓(𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o)))
31 ismkv 7141 . . . . . 6 (𝐴 ∈ V → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
3230, 31anbi12d 473 . . . . 5 (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔ (∀𝑓(𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
33 19.26 1479 . . . . 5 (∀𝑓((𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) ↔ (∀𝑓(𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
3432, 33bitr4di 198 . . . 4 (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔ ∀𝑓((𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
35 jcab 603 . . . . 5 ((𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) ↔ ((𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
3635albii 1468 . . . 4 (∀𝑓(𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))) ↔ ∀𝑓((𝑓:𝐴⟶2oDECID𝑥𝐴 (𝑓𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅))))
3734, 36bitr4di 198 . . 3 (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔ ∀𝑓(𝑓:𝐴⟶2o → (DECID𝑥𝐴 (𝑓𝑥) = 1o ∧ (¬ ∀𝑥𝐴 (𝑓𝑥) = 1o → ∃𝑥𝐴 (𝑓𝑥) = ∅)))))
3828, 29, 373bitr4d 220 . 2 (𝐴 ∈ V → (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov)))
391, 3, 38pm5.21nii 704 1 (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834  wal 1351   = wceq 1353  wcel 2146  wral 2453  wrex 2454  Vcvv 2735  c0 3420  wf 5204  cfv 5208  1oc1o 6400  2oc2o 6401  Omnicomni 7122  Markovcmarkov 7139  WOmnicwomni 7151
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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-nul 4124
This theorem depends on definitions:  df-bi 117  df-dc 835  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-v 2737  df-dif 3129  df-un 3131  df-nul 3421  df-sn 3595  df-suc 4365  df-fn 5211  df-f 5212  df-1o 6407  df-omni 7123  df-markov 7140  df-womni 7152
This theorem is referenced by:  lpowlpo  7156
  Copyright terms: Public domain W3C validator