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

Theorem dfac4 9149
Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Axiom AC of [BellMachover] p. 488. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004.) (Revised by Mario Carneiro, 26-Jun-2015.)
Assertion
Ref Expression
dfac4 (CHOICE ↔ ∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
Distinct variable group:   𝑥,𝑓,𝑧

Proof of Theorem dfac4
Dummy variables 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac3 9148 . 2 (CHOICE ↔ ∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧))
2 fveq1 6332 . . . . . . . . 9 (𝑓 = 𝑦 → (𝑓𝑧) = (𝑦𝑧))
32eleq1d 2835 . . . . . . . 8 (𝑓 = 𝑦 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑦𝑧) ∈ 𝑧))
43imbi2d 329 . . . . . . 7 (𝑓 = 𝑦 → ((𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
54ralbidv 3135 . . . . . 6 (𝑓 = 𝑦 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
65cbvexvw 2126 . . . . 5 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
7 fvex 6344 . . . . . . . . 9 (𝑦𝑤) ∈ V
8 eqid 2771 . . . . . . . . 9 (𝑤𝑥 ↦ (𝑦𝑤)) = (𝑤𝑥 ↦ (𝑦𝑤))
97, 8fnmpti 6161 . . . . . . . 8 (𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥
10 fveq2 6333 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (𝑦𝑤) = (𝑦𝑧))
11 fvex 6344 . . . . . . . . . . . . 13 (𝑦𝑧) ∈ V
1210, 8, 11fvmpt 6426 . . . . . . . . . . . 12 (𝑧𝑥 → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) = (𝑦𝑧))
1312eleq1d 2835 . . . . . . . . . . 11 (𝑧𝑥 → (((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧 ↔ (𝑦𝑧) ∈ 𝑧))
1413imbi2d 329 . . . . . . . . . 10 (𝑧𝑥 → ((𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
1514ralbiia 3128 . . . . . . . . 9 (∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
1615anbi2i 609 . . . . . . . 8 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) ↔ ((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
179, 16mpbiran 688 . . . . . . 7 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
18 fvrn0 6359 . . . . . . . . . . 11 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅})
1918rgenw 3073 . . . . . . . . . 10 𝑤𝑥 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅})
208fmpt 6525 . . . . . . . . . 10 (∀𝑤𝑥 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅}) ↔ (𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅}))
2119, 20mpbi 220 . . . . . . . . 9 (𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅})
22 vex 3354 . . . . . . . . 9 𝑥 ∈ V
23 vex 3354 . . . . . . . . . . 11 𝑦 ∈ V
2423rnex 7251 . . . . . . . . . 10 ran 𝑦 ∈ V
25 p0ex 4985 . . . . . . . . . 10 {∅} ∈ V
2624, 25unex 7107 . . . . . . . . 9 (ran 𝑦 ∪ {∅}) ∈ V
27 fex2 7272 . . . . . . . . 9 (((𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅}) ∧ 𝑥 ∈ V ∧ (ran 𝑦 ∪ {∅}) ∈ V) → (𝑤𝑥 ↦ (𝑦𝑤)) ∈ V)
2821, 22, 26, 27mp3an 1572 . . . . . . . 8 (𝑤𝑥 ↦ (𝑦𝑤)) ∈ V
29 fneq1 6118 . . . . . . . . 9 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (𝑓 Fn 𝑥 ↔ (𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥))
30 fveq1 6332 . . . . . . . . . . . 12 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (𝑓𝑧) = ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧))
3130eleq1d 2835 . . . . . . . . . . 11 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑓𝑧) ∈ 𝑧 ↔ ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧))
3231imbi2d 329 . . . . . . . . . 10 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)))
3332ralbidv 3135 . . . . . . . . 9 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)))
3429, 33anbi12d 616 . . . . . . . 8 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) ↔ ((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧))))
3528, 34spcev 3451 . . . . . . 7 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
3617, 35sylbir 225 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
3736exlimiv 2010 . . . . 5 (∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
386, 37sylbi 207 . . . 4 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
39 exsimpr 1947 . . . 4 (∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) → ∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧))
4038, 39impbii 199 . . 3 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
4140albii 1895 . 2 (∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
421, 41bitri 264 1 (CHOICE ↔ ∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wal 1629   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  Vcvv 3351  cun 3721  c0 4063  {csn 4317  cmpt 4864  ran crn 5251   Fn wfn 6025  wf 6026  cfv 6030  CHOICEwac 9142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-fv 6038  df-ac 9143
This theorem is referenced by:  dfac5  9155  dfacacn  9169  ac5  9505
  Copyright terms: Public domain W3C validator