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

Theorem dfac4 10162
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 10161 . 2 (CHOICE ↔ ∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧))
2 fveq1 6905 . . . . . . . . 9 (𝑓 = 𝑦 → (𝑓𝑧) = (𝑦𝑧))
32eleq1d 2826 . . . . . . . 8 (𝑓 = 𝑦 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑦𝑧) ∈ 𝑧))
43imbi2d 340 . . . . . . 7 (𝑓 = 𝑦 → ((𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
54ralbidv 3178 . . . . . 6 (𝑓 = 𝑦 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
65cbvexvw 2036 . . . . 5 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
7 fvex 6919 . . . . . . . . 9 (𝑦𝑤) ∈ V
8 eqid 2737 . . . . . . . . 9 (𝑤𝑥 ↦ (𝑦𝑤)) = (𝑤𝑥 ↦ (𝑦𝑤))
97, 8fnmpti 6711 . . . . . . . 8 (𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥
10 fveq2 6906 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (𝑦𝑤) = (𝑦𝑧))
11 fvex 6919 . . . . . . . . . . . . 13 (𝑦𝑧) ∈ V
1210, 8, 11fvmpt 7016 . . . . . . . . . . . 12 (𝑧𝑥 → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) = (𝑦𝑧))
1312eleq1d 2826 . . . . . . . . . . 11 (𝑧𝑥 → (((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧 ↔ (𝑦𝑧) ∈ 𝑧))
1413imbi2d 340 . . . . . . . . . 10 (𝑧𝑥 → ((𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
1514ralbiia 3091 . . . . . . . . 9 (∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
1615anbi2i 623 . . . . . . . 8 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) ↔ ((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧)))
179, 16mpbiran 709 . . . . . . 7 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧))
18 fvrn0 6936 . . . . . . . . . . 11 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅})
1918rgenw 3065 . . . . . . . . . 10 𝑤𝑥 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅})
208fmpt 7130 . . . . . . . . . 10 (∀𝑤𝑥 (𝑦𝑤) ∈ (ran 𝑦 ∪ {∅}) ↔ (𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅}))
2119, 20mpbi 230 . . . . . . . . 9 (𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅})
22 vex 3484 . . . . . . . . 9 𝑥 ∈ V
23 vex 3484 . . . . . . . . . . 11 𝑦 ∈ V
2423rnex 7932 . . . . . . . . . 10 ran 𝑦 ∈ V
25 p0ex 5384 . . . . . . . . . 10 {∅} ∈ V
2624, 25unex 7764 . . . . . . . . 9 (ran 𝑦 ∪ {∅}) ∈ V
27 fex2 7958 . . . . . . . . 9 (((𝑤𝑥 ↦ (𝑦𝑤)):𝑥⟶(ran 𝑦 ∪ {∅}) ∧ 𝑥 ∈ V ∧ (ran 𝑦 ∪ {∅}) ∈ V) → (𝑤𝑥 ↦ (𝑦𝑤)) ∈ V)
2821, 22, 26, 27mp3an 1463 . . . . . . . 8 (𝑤𝑥 ↦ (𝑦𝑤)) ∈ V
29 fneq1 6659 . . . . . . . . 9 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (𝑓 Fn 𝑥 ↔ (𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥))
30 fveq1 6905 . . . . . . . . . . . 12 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (𝑓𝑧) = ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧))
3130eleq1d 2826 . . . . . . . . . . 11 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑓𝑧) ∈ 𝑧 ↔ ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧))
3231imbi2d 340 . . . . . . . . . 10 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)))
3332ralbidv 3178 . . . . . . . . 9 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)))
3429, 33anbi12d 632 . . . . . . . 8 (𝑓 = (𝑤𝑥 ↦ (𝑦𝑤)) → ((𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) ↔ ((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧))))
3528, 34spcev 3606 . . . . . . 7 (((𝑤𝑥 ↦ (𝑦𝑤)) Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → ((𝑤𝑥 ↦ (𝑦𝑤))‘𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
3617, 35sylbir 235 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
3736exlimiv 1930 . . . . 5 (∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → (𝑦𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
386, 37sylbi 217 . . . 4 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
39 exsimpr 1869 . . . 4 (∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) → ∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧))
4038, 39impbii 209 . . 3 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
4140albii 1819 . 2 (∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ ∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
421, 41bitri 275 1 (CHOICE ↔ ∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  Vcvv 3480  cun 3949  c0 4333  {csn 4626  cmpt 5225  ran crn 5686   Fn wfn 6556  wf 6557  cfv 6561  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-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-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-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:  dfac5  10169  dfacacn  10182  ac5  10517
  Copyright terms: Public domain W3C validator