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

Theorem dfac4 8801
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 8800 . 2 (CHOICE ↔ ∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧))
2 fveq1 6083 . . . . . . . . 9 (𝑓 = 𝑦 → (𝑓𝑧) = (𝑦𝑧))
32eleq1d 2667 . . . . . . . 8 (𝑓 = 𝑦 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑦𝑧) ∈ 𝑧))
43imbi2d 328 . . . . . . 7 (𝑓 = 𝑦 → ((𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
54ralbidv 2964 . . . . . 6 (𝑓 = 𝑦 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
65cbvexv 2257 . . . . 5 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
7 fvex 6094 . . . . . . . . 9 (𝑦𝑤) ∈ V
8 eqid 2605 . . . . . . . . 9 (𝑤𝑥 ↦ (𝑦𝑤)) = (𝑤𝑥 ↦ (𝑦𝑤))
97, 8fnmpti 5917 . . . . . . . 8 (𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥
10 fveq2 6084 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (𝑦𝑤) = (𝑦𝑧))
11 fvex 6094 . . . . . . . . . . . . 13 (𝑦𝑧) ∈ V
1210, 8, 11fvmpt 6172 . . . . . . . . . . . 12 (𝑧𝑥 → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) = (𝑦𝑧))
1312eleq1d 2667 . . . . . . . . . . 11 (𝑧𝑥 → (((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧 ↔ (𝑦𝑧) ∈ 𝑧))
1413imbi2d 328 . . . . . . . . . 10 (𝑧𝑥 → ((𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
1514ralbiia 2957 . . . . . . . . 9 (∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
1615anbi2i 725 . . . . . . . 8 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) ↔ ((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
179, 16mpbiran 954 . . . . . . 7 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
18 fvrn0 6107 . . . . . . . . . . 11 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅})
1918rgenw 2903 . . . . . . . . . 10 𝑤𝑥 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅})
208fmpt 6270 . . . . . . . . . 10 (∀𝑤𝑥 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅}) ↔ (𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅}))
2119, 20mpbi 218 . . . . . . . . 9 (𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅})
22 vex 3171 . . . . . . . . 9 𝑥 ∈ V
23 vex 3171 . . . . . . . . . . 11 𝑦 ∈ V
2423rnex 6965 . . . . . . . . . 10 ran 𝑦 ∈ V
25 p0ex 4770 . . . . . . . . . 10 {∅} ∈ V
2624, 25unex 6827 . . . . . . . . 9 (ran 𝑦 ∪ {∅}) ∈ V
27 fex2 6987 . . . . . . . . 9 (((𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅}) ∧ 𝑥 ∈ V ∧ (ran 𝑦 ∪ {∅}) ∈ V) → (𝑤𝑥 ↦ (𝑦𝑤)) ∈ V)
2821, 22, 26, 27mp3an 1415 . . . . . . . 8 (𝑤𝑥 ↦ (𝑦𝑤)) ∈ V
29 fneq1 5875 . . . . . . . . 9 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (𝑓 Fn 𝑥 ↔ (𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥))
30 fveq1 6083 . . . . . . . . . . . 12 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (𝑓𝑧) = ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧))
3130eleq1d 2667 . . . . . . . . . . 11 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑓𝑧) ∈ 𝑧 ↔ ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧))
3231imbi2d 328 . . . . . . . . . 10 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)))
3332ralbidv 2964 . . . . . . . . 9 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)))
3429, 33anbi12d 742 . . . . . . . 8 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) ↔ ((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧))))
3528, 34spcev 3268 . . . . . . 7 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
3617, 35sylbir 223 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
3736exlimiv 1843 . . . . 5 (∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
386, 37sylbi 205 . . . 4 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
39 exsimpr 1782 . . . 4 (∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) → ∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧))
4038, 39impbii 197 . . 3 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
4140albii 1735 . 2 (∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
421, 41bitri 262 1 (CHOICE ↔ ∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wal 1472   = wceq 1474  wex 1694  wcel 1975  wne 2775  wral 2891  Vcvv 3168  cun 3533  c0 3869  {csn 4120  cmpt 4633  ran crn 5025   Fn wfn 5781  wf 5782  cfv 5786  CHOICEwac 8794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-sbc 3398  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-mpt 4635  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-fv 5794  df-ac 8795
This theorem is referenced by:  dfac5  8807  dfacacn  8819  ac5  9155
  Copyright terms: Public domain W3C validator