MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfackm Structured version   Visualization version   GIF version

Theorem dfackm 10207
Description: Equivalence of the Axiom of Choice and Maes' AC ackm 10505. The proof consists of lemmas kmlem1 10191 through kmlem16 10206 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e., replacing dfac5 10169 with biid 261) establishes the AC equivalence shown by Maes' writeup. The left-hand-side AC shown here was chosen because it is shorter to display. (Contributed by NM, 13-Apr-2004.) (Revised by Mario Carneiro, 17-May-2015.)
Assertion
Ref Expression
dfackm (CHOICE ↔ ∀𝑥𝑦𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))))
Distinct variable group:   𝑥,𝑦,𝑧,𝑣,𝑢

Proof of Theorem dfackm
Dummy variables 𝑤 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac5 10169 . 2 (CHOICE ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
2 eqid 2737 . . . . 5 {𝑡 ∣ ∃𝑥 𝑡 = ( (𝑥 ∖ {}))} = {𝑡 ∣ ∃𝑥 𝑡 = ( (𝑥 ∖ {}))}
32kmlem13 10203 . . . 4 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ∀𝑥(¬ ∃𝑧𝑥𝑣𝑧𝑤𝑥 (𝑧𝑤𝑣 ∈ (𝑧𝑤)) → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
4 kmlem8 10198 . . . . 5 ((¬ ∃𝑧𝑥𝑣𝑧𝑤𝑥 (𝑧𝑤𝑣 ∈ (𝑧𝑤)) → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ (∃𝑧𝑥𝑣𝑧𝑤𝑥 (𝑧𝑤𝑣 ∈ (𝑧𝑤)) ∨ ∃𝑦𝑦𝑥 ∧ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
54albii 1819 . . . 4 (∀𝑥(¬ ∃𝑧𝑥𝑣𝑧𝑤𝑥 (𝑧𝑤𝑣 ∈ (𝑧𝑤)) → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ∀𝑥(∃𝑧𝑥𝑣𝑧𝑤𝑥 (𝑧𝑤𝑣 ∈ (𝑧𝑤)) ∨ ∃𝑦𝑦𝑥 ∧ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
63, 5bitri 275 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ∀𝑥(∃𝑧𝑥𝑣𝑧𝑤𝑥 (𝑧𝑤𝑣 ∈ (𝑧𝑤)) ∨ ∃𝑦𝑦𝑥 ∧ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
7 df-ne 2941 . . . . . . . . 9 (𝑦𝑣 ↔ ¬ 𝑦 = 𝑣)
87bicomi 224 . . . . . . . 8 𝑦 = 𝑣𝑦𝑣)
98anbi2i 623 . . . . . . 7 ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ↔ (𝑣𝑥𝑦𝑣))
109anbi1i 624 . . . . . 6 (((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣) ↔ ((𝑣𝑥𝑦𝑣) ∧ 𝑧𝑣))
1110imbi2i 336 . . . . 5 ((𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣)) ↔ (𝑧𝑦 → ((𝑣𝑥𝑦𝑣) ∧ 𝑧𝑣)))
12 biid 261 . . . . 5 ((𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
13 biid 261 . . . . 5 (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
1411, 12, 13kmlem16 10206 . . . 4 ((∃𝑧𝑥𝑣𝑧𝑤𝑥 (𝑧𝑤𝑣 ∈ (𝑧𝑤)) ∨ ∃𝑦𝑦𝑥 ∧ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ∃𝑦𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))))
1514albii 1819 . . 3 (∀𝑥(∃𝑧𝑥𝑣𝑧𝑤𝑥 (𝑧𝑤𝑣 ∈ (𝑧𝑤)) ∨ ∃𝑦𝑦𝑥 ∧ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ∀𝑥𝑦𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))))
166, 15bitri 275 . 2 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ∀𝑥𝑦𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))))
171, 16bitri 275 1 (CHOICE ↔ ∀𝑥𝑦𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  wal 1538   = wceq 1540  wex 1779  wcel 2108  ∃!weu 2568  {cab 2714  wne 2940  wral 3061  wrex 3070  cdif 3948  cin 3950  c0 4333  {csn 4626   cuni 4907  CHOICEwac 10155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ac 10156
This theorem is referenced by:  axac3  10504  ackm  10505  axac2  10506
  Copyright terms: Public domain W3C validator