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

Theorem dfac5 9543
 Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Theorem 6M(4) of [Enderton] p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 17-May-2015.)
Assertion
Ref Expression
dfac5 (CHOICE ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
Distinct variable group:   𝑥,𝑧,𝑦,𝑤,𝑣

Proof of Theorem dfac5
Dummy variables 𝑓 𝑢 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac4 9537 . . 3 (CHOICE ↔ ∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤)))
2 neeq1 3052 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (𝑧 ≠ ∅ ↔ 𝑤 ≠ ∅))
32cbvralvw 3399 . . . . . . . . . . . 12 (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑤𝑥 𝑤 ≠ ∅)
43anbi2i 625 . . . . . . . . . . 11 ((∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ ∀𝑧𝑥 𝑧 ≠ ∅) ↔ (∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ ∀𝑤𝑥 𝑤 ≠ ∅))
5 r19.26 3140 . . . . . . . . . . 11 (∀𝑤𝑥 ((𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ 𝑤 ≠ ∅) ↔ (∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ ∀𝑤𝑥 𝑤 ≠ ∅))
64, 5bitr4i 281 . . . . . . . . . 10 ((∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ ∀𝑧𝑥 𝑧 ≠ ∅) ↔ ∀𝑤𝑥 ((𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ 𝑤 ≠ ∅))
7 pm3.35 802 . . . . . . . . . . . 12 ((𝑤 ≠ ∅ ∧ (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤)) → (𝑓𝑤) ∈ 𝑤)
87ancoms 462 . . . . . . . . . . 11 (((𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ 𝑤 ≠ ∅) → (𝑓𝑤) ∈ 𝑤)
98ralimi 3131 . . . . . . . . . 10 (∀𝑤𝑥 ((𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ 𝑤 ≠ ∅) → ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤)
106, 9sylbi 220 . . . . . . . . 9 ((∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ ∀𝑧𝑥 𝑧 ≠ ∅) → ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤)
11 r19.26 3140 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) ↔ (∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤 ∧ ∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)))
12 elin 3900 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ (𝑣𝑧𝑣 ∈ ran 𝑓))
13 fvelrnb 6705 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 Fn 𝑥 → (𝑣 ∈ ran 𝑓 ↔ ∃𝑡𝑥 (𝑓𝑡) = 𝑣))
1413biimpac 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ ran 𝑓𝑓 Fn 𝑥) → ∃𝑡𝑥 (𝑓𝑡) = 𝑣)
15 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑡 → (𝑓𝑤) = (𝑓𝑡))
16 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑡𝑤 = 𝑡)
1715, 16eleq12d 2887 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑡 → ((𝑓𝑤) ∈ 𝑤 ↔ (𝑓𝑡) ∈ 𝑡))
18 neeq2 3053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑡 → (𝑧𝑤𝑧𝑡))
19 ineq2 4136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑡 → (𝑧𝑤) = (𝑧𝑡))
2019eqeq1d 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑡 → ((𝑧𝑤) = ∅ ↔ (𝑧𝑡) = ∅))
2118, 20imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑡 → ((𝑧𝑤 → (𝑧𝑤) = ∅) ↔ (𝑧𝑡 → (𝑧𝑡) = ∅)))
2217, 21anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑡 → (((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) ↔ ((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡 → (𝑧𝑡) = ∅))))
2322rspcv 3569 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡𝑥 → (∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) → ((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡 → (𝑧𝑡) = ∅))))
24 minel 4376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡) = ∅) → ¬ (𝑓𝑡) ∈ 𝑧)
2524ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓𝑡) ∈ 𝑡 → ((𝑧𝑡) = ∅ → ¬ (𝑓𝑡) ∈ 𝑧))
2625imim2d 57 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑡) ∈ 𝑡 → ((𝑧𝑡 → (𝑧𝑡) = ∅) → (𝑧𝑡 → ¬ (𝑓𝑡) ∈ 𝑧)))
2726imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡 → (𝑧𝑡) = ∅)) → (𝑧𝑡 → ¬ (𝑓𝑡) ∈ 𝑧))
2827necon4ad 3009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡 → (𝑧𝑡) = ∅)) → ((𝑓𝑡) ∈ 𝑧𝑧 = 𝑡))
29 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑡) = 𝑣 → ((𝑓𝑡) ∈ 𝑧𝑣𝑧))
3029biimpar 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓𝑡) = 𝑣𝑣𝑧) → (𝑓𝑡) ∈ 𝑧)
3128, 30impel 509 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡 → (𝑧𝑡) = ∅)) ∧ ((𝑓𝑡) = 𝑣𝑣𝑧)) → 𝑧 = 𝑡)
32 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑡 → (𝑓𝑧) = (𝑓𝑡))
33 eqeq2 2813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑡) = 𝑣 → ((𝑓𝑧) = (𝑓𝑡) ↔ (𝑓𝑧) = 𝑣))
34 eqcom 2808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑧) = 𝑣𝑣 = (𝑓𝑧))
3533, 34syl6bb 290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑡) = 𝑣 → ((𝑓𝑧) = (𝑓𝑡) ↔ 𝑣 = (𝑓𝑧)))
3632, 35syl5ib 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓𝑡) = 𝑣 → (𝑧 = 𝑡𝑣 = (𝑓𝑧)))
3736ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡 → (𝑧𝑡) = ∅)) ∧ ((𝑓𝑡) = 𝑣𝑣𝑧)) → (𝑧 = 𝑡𝑣 = (𝑓𝑧)))
3831, 37mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡 → (𝑧𝑡) = ∅)) ∧ ((𝑓𝑡) = 𝑣𝑣𝑧)) → 𝑣 = (𝑓𝑧))
3938exp32 424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓𝑡) ∈ 𝑡 ∧ (𝑧𝑡 → (𝑧𝑡) = ∅)) → ((𝑓𝑡) = 𝑣 → (𝑣𝑧𝑣 = (𝑓𝑧))))
4023, 39syl6com 37 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) → (𝑡𝑥 → ((𝑓𝑡) = 𝑣 → (𝑣𝑧𝑣 = (𝑓𝑧)))))
4140com14 96 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣𝑧 → (𝑡𝑥 → ((𝑓𝑡) = 𝑣 → (∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) → 𝑣 = (𝑓𝑧)))))
4241rexlimdv 3245 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣𝑧 → (∃𝑡𝑥 (𝑓𝑡) = 𝑣 → (∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) → 𝑣 = (𝑓𝑧))))
4314, 42syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝑧 → ((𝑣 ∈ ran 𝑓𝑓 Fn 𝑥) → (∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) → 𝑣 = (𝑓𝑧))))
4443expd 419 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑧 → (𝑣 ∈ ran 𝑓 → (𝑓 Fn 𝑥 → (∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) → 𝑣 = (𝑓𝑧)))))
4544com4t 93 . . . . . . . . . . . . . . . . . . . 20 (𝑓 Fn 𝑥 → (∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅)) → (𝑣𝑧 → (𝑣 ∈ ran 𝑓𝑣 = (𝑓𝑧)))))
4645imp4b 425 . . . . . . . . . . . . . . . . . . 19 ((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅))) → ((𝑣𝑧𝑣 ∈ ran 𝑓) → 𝑣 = (𝑓𝑧)))
4712, 46syl5bi 245 . . . . . . . . . . . . . . . . . 18 ((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 ((𝑓𝑤) ∈ 𝑤 ∧ (𝑧𝑤 → (𝑧𝑤) = ∅))) → (𝑣 ∈ (𝑧 ∩ ran 𝑓) → 𝑣 = (𝑓𝑧)))
4811, 47sylan2br 597 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑥 ∧ (∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤 ∧ ∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅))) → (𝑣 ∈ (𝑧 ∩ ran 𝑓) → 𝑣 = (𝑓𝑧)))
4948anassrs 471 . . . . . . . . . . . . . . . 16 (((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ ∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → (𝑣 ∈ (𝑧 ∩ ran 𝑓) → 𝑣 = (𝑓𝑧)))
5049adantlr 714 . . . . . . . . . . . . . . 15 ((((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ 𝑧𝑥) ∧ ∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → (𝑣 ∈ (𝑧 ∩ ran 𝑓) → 𝑣 = (𝑓𝑧)))
51 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → (𝑓𝑤) = (𝑓𝑧))
52 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧𝑤 = 𝑧)
5351, 52eleq12d 2887 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ((𝑓𝑤) ∈ 𝑤 ↔ (𝑓𝑧) ∈ 𝑧))
5453rspcv 3569 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑥 → (∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤 → (𝑓𝑧) ∈ 𝑧))
55 fnfvelrn 6829 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 Fn 𝑥𝑧𝑥) → (𝑓𝑧) ∈ ran 𝑓)
5655expcom 417 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑥 → (𝑓 Fn 𝑥 → (𝑓𝑧) ∈ ran 𝑓))
5754, 56anim12d 611 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑥 → ((∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤𝑓 Fn 𝑥) → ((𝑓𝑧) ∈ 𝑧 ∧ (𝑓𝑧) ∈ ran 𝑓)))
58 elin 3900 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑧) ∈ (𝑧 ∩ ran 𝑓) ↔ ((𝑓𝑧) ∈ 𝑧 ∧ (𝑓𝑧) ∈ ran 𝑓))
5957, 58syl6ibr 255 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑥 → ((∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤𝑓 Fn 𝑥) → (𝑓𝑧) ∈ (𝑧 ∩ ran 𝑓)))
6059expd 419 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → (∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤 → (𝑓 Fn 𝑥 → (𝑓𝑧) ∈ (𝑧 ∩ ran 𝑓))))
6160com13 88 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑥 → (∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤 → (𝑧𝑥 → (𝑓𝑧) ∈ (𝑧 ∩ ran 𝑓))))
6261imp31 421 . . . . . . . . . . . . . . . . 17 (((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ 𝑧𝑥) → (𝑓𝑧) ∈ (𝑧 ∩ ran 𝑓))
63 eleq1 2880 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑓𝑧) → (𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ (𝑓𝑧) ∈ (𝑧 ∩ ran 𝑓)))
6462, 63syl5ibrcom 250 . . . . . . . . . . . . . . . 16 (((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ 𝑧𝑥) → (𝑣 = (𝑓𝑧) → 𝑣 ∈ (𝑧 ∩ ran 𝑓)))
6564adantr 484 . . . . . . . . . . . . . . 15 ((((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ 𝑧𝑥) ∧ ∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → (𝑣 = (𝑓𝑧) → 𝑣 ∈ (𝑧 ∩ ran 𝑓)))
6650, 65impbid 215 . . . . . . . . . . . . . 14 ((((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ 𝑧𝑥) ∧ ∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → (𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = (𝑓𝑧)))
6766ex 416 . . . . . . . . . . . . 13 (((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ 𝑧𝑥) → (∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) → (𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = (𝑓𝑧))))
6867alrimdv 1930 . . . . . . . . . . . 12 (((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ 𝑧𝑥) → (∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) → ∀𝑣(𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = (𝑓𝑧))))
69 fvex 6662 . . . . . . . . . . . . . 14 (𝑓𝑧) ∈ V
70 eqeq2 2813 . . . . . . . . . . . . . . . 16 ( = (𝑓𝑧) → (𝑣 = 𝑣 = (𝑓𝑧)))
7170bibi2d 346 . . . . . . . . . . . . . . 15 ( = (𝑓𝑧) → ((𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = ) ↔ (𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = (𝑓𝑧))))
7271albidv 1921 . . . . . . . . . . . . . 14 ( = (𝑓𝑧) → (∀𝑣(𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = ) ↔ ∀𝑣(𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = (𝑓𝑧))))
7369, 72spcev 3558 . . . . . . . . . . . . 13 (∀𝑣(𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = (𝑓𝑧)) → ∃𝑣(𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = ))
74 eu6 2637 . . . . . . . . . . . . 13 (∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ ∃𝑣(𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = ))
7573, 74sylibr 237 . . . . . . . . . . . 12 (∀𝑣(𝑣 ∈ (𝑧 ∩ ran 𝑓) ↔ 𝑣 = (𝑓𝑧)) → ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓))
7668, 75syl6 35 . . . . . . . . . . 11 (((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) ∧ 𝑧𝑥) → (∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) → ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓)))
7776ralimdva 3147 . . . . . . . . . 10 ((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤) → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) → ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓)))
7877ex 416 . . . . . . . . 9 (𝑓 Fn 𝑥 → (∀𝑤𝑥 (𝑓𝑤) ∈ 𝑤 → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) → ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓))))
7910, 78syl5 34 . . . . . . . 8 (𝑓 Fn 𝑥 → ((∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) ∧ ∀𝑧𝑥 𝑧 ≠ ∅) → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) → ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓))))
8079expd 419 . . . . . . 7 (𝑓 Fn 𝑥 → (∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤) → (∀𝑧𝑥 𝑧 ≠ ∅ → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) → ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓)))))
8180imp4b 425 . . . . . 6 ((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤)) → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓)))
82 vex 3447 . . . . . . . 8 𝑓 ∈ V
8382rnex 7603 . . . . . . 7 ran 𝑓 ∈ V
84 ineq2 4136 . . . . . . . . . 10 (𝑦 = ran 𝑓 → (𝑧𝑦) = (𝑧 ∩ ran 𝑓))
8584eleq2d 2878 . . . . . . . . 9 (𝑦 = ran 𝑓 → (𝑣 ∈ (𝑧𝑦) ↔ 𝑣 ∈ (𝑧 ∩ ran 𝑓)))
8685eubidv 2650 . . . . . . . 8 (𝑦 = ran 𝑓 → (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓)))
8786ralbidv 3165 . . . . . . 7 (𝑦 = ran 𝑓 → (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓)))
8883, 87spcev 3558 . . . . . 6 (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ ran 𝑓) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
8981, 88syl6 35 . . . . 5 ((𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤)) → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
9089exlimiv 1931 . . . 4 (∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤)) → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
9190alimi 1813 . . 3 (∀𝑥𝑓(𝑓 Fn 𝑥 ∧ ∀𝑤𝑥 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤)) → ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
921, 91sylbi 220 . 2 (CHOICE → ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
93 eqid 2801 . . . . 5 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
94 eqid 2801 . . . . 5 ( {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ∩ 𝑦) = ( {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ∩ 𝑦)
95 biid 264 . . . . 5 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
9693, 94, 95dfac5lem5 9542 . . . 4 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ∃𝑓𝑤 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤))
9796alrimiv 1928 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ∀𝑓𝑤 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤))
98 dfac3 9536 . . 3 (CHOICE ↔ ∀𝑓𝑤 (𝑤 ≠ ∅ → (𝑓𝑤) ∈ 𝑤))
9997, 98sylibr 237 . 2 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → CHOICE)
10092, 99impbii 212 1 (CHOICE ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2112  ∃!weu 2631  {cab 2779   ≠ wne 2990  ∀wral 3109  ∃wrex 3110   ∩ cin 3883  ∅c0 4246  {csn 4528  ∪ cuni 4803   × cxp 5521  ran crn 5524   Fn wfn 6323  ‘cfv 6328  CHOICEwac 9530 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336  df-ac 9531 This theorem is referenced by:  dfackm  9581  ac8  9907
 Copyright terms: Public domain W3C validator