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

Theorem dfac2b 10067
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies our Axiom of Choice (in the form of ac3 10399). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq 9535 and preleq 9553 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a 10066.) (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by AV, 16-Jun-2022.)
Assertion
Ref Expression
dfac2b (CHOICE → ∀𝑥𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
Distinct variable group:   𝑥,𝑧,𝑦,𝑤,𝑣

Proof of Theorem dfac2b
Dummy variables 𝑓 𝑢 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac3 10058 . 2 (CHOICE ↔ ∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧))
2 nfra1 3268 . . . . . 6 𝑧𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)
3 rsp 3231 . . . . . . . . . . . 12 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑧𝑥 → (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
4 equid 2016 . . . . . . . . . . . . . . . . . 18 𝑧 = 𝑧
5 neeq1 3007 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
6 eqeq1 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑧 → (𝑢 = 𝑧𝑧 = 𝑧))
75, 6anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) ↔ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)))
87rspcev 3582 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑥 ∧ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)) → ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
94, 8mpanr2 703 . . . . . . . . . . . . . . . . 17 ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
10 fveq2 6843 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑧 → (𝑓𝑢) = (𝑓𝑧))
1110preq1d 4701 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑧 → {(𝑓𝑢), 𝑢} = {(𝑓𝑧), 𝑢})
12 preq2 4696 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑧 → {(𝑓𝑧), 𝑢} = {(𝑓𝑧), 𝑧})
1311, 12eqtr2d 2778 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑧 → {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢})
1413anim2i 618 . . . . . . . . . . . . . . . . . 18 ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
1514reximi 3088 . . . . . . . . . . . . . . . . 17 (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
169, 15syl 17 . . . . . . . . . . . . . . . 16 ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
17 prex 5390 . . . . . . . . . . . . . . . . 17 {(𝑓𝑧), 𝑧} ∈ V
18 eqeq1 2741 . . . . . . . . . . . . . . . . . . 19 (𝑔 = {(𝑓𝑧), 𝑧} → (𝑔 = {(𝑓𝑢), 𝑢} ↔ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
1918anbi2d 630 . . . . . . . . . . . . . . . . . 18 (𝑔 = {(𝑓𝑧), 𝑧} → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢})))
2019rexbidv 3176 . . . . . . . . . . . . . . . . 17 (𝑔 = {(𝑓𝑧), 𝑧} → (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) ↔ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢})))
2117, 20elab 3631 . . . . . . . . . . . . . . . 16 ({(𝑓𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ↔ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
2216, 21sylibr 233 . . . . . . . . . . . . . . 15 ((𝑧𝑥𝑧 ≠ ∅) → {(𝑓𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})})
23 vex 3450 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
2423prid2 4725 . . . . . . . . . . . . . . . 16 𝑧 ∈ {(𝑓𝑧), 𝑧}
25 fvex 6856 . . . . . . . . . . . . . . . . 17 (𝑓𝑧) ∈ V
2625prid1 4724 . . . . . . . . . . . . . . . 16 (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧}
2724, 26pm3.2i 472 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑓𝑧), 𝑧} ∧ (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧})
28 eleq2 2827 . . . . . . . . . . . . . . . . 17 (𝑣 = {(𝑓𝑧), 𝑧} → (𝑧𝑣𝑧 ∈ {(𝑓𝑧), 𝑧}))
29 eleq2 2827 . . . . . . . . . . . . . . . . 17 (𝑣 = {(𝑓𝑧), 𝑧} → ((𝑓𝑧) ∈ 𝑣 ↔ (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧}))
3028, 29anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑣 = {(𝑓𝑧), 𝑧} → ((𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣) ↔ (𝑧 ∈ {(𝑓𝑧), 𝑧} ∧ (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧})))
3130rspcev 3582 . . . . . . . . . . . . . . 15 (({(𝑓𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ∧ (𝑧 ∈ {(𝑓𝑧), 𝑧} ∧ (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧})) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣))
3222, 27, 31sylancl 587 . . . . . . . . . . . . . 14 ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣))
33 eleq1 2826 . . . . . . . . . . . . . . . 16 (𝑤 = (𝑓𝑧) → (𝑤𝑧 ↔ (𝑓𝑧) ∈ 𝑧))
34 eleq1 2826 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝑓𝑧) → (𝑤𝑣 ↔ (𝑓𝑧) ∈ 𝑣))
3534anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝑓𝑧) → ((𝑧𝑣𝑤𝑣) ↔ (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣)))
3635rexbidv 3176 . . . . . . . . . . . . . . . 16 (𝑤 = (𝑓𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣)))
3733, 36anbi12d 632 . . . . . . . . . . . . . . 15 (𝑤 = (𝑓𝑧) → ((𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ↔ ((𝑓𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣))))
3825, 37spcev 3566 . . . . . . . . . . . . . 14 (((𝑓𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣)) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
3932, 38sylan2 594 . . . . . . . . . . . . 13 (((𝑓𝑧) ∈ 𝑧 ∧ (𝑧𝑥𝑧 ≠ ∅)) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
4039ex 414 . . . . . . . . . . . 12 ((𝑓𝑧) ∈ 𝑧 → ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
413, 40syl8 76 . . . . . . . . . . 11 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑧𝑥 → (𝑧 ≠ ∅ → ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))))
4241impd 412 . . . . . . . . . 10 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑥𝑧 ≠ ∅) → ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))))
4342pm2.43d 53 . . . . . . . . 9 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
44 df-rex 3075 . . . . . . . . . . . . 13 (∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) ↔ ∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ∧ (𝑧𝑣𝑤𝑣)))
45 vex 3450 . . . . . . . . . . . . . . . . . . 19 𝑣 ∈ V
46 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑣 → (𝑔 = {(𝑓𝑢), 𝑢} ↔ 𝑣 = {(𝑓𝑢), 𝑢}))
4746anbi2d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑣 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢})))
4847rexbidv 3176 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑣 → (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) ↔ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢})))
4945, 48elab 3631 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ↔ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢}))
50 neeq1 3007 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑢 → (𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅))
51 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑢 → (𝑓𝑧) = (𝑓𝑢))
5251eleq1d 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑢 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝑢) ∈ 𝑧))
53 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑢 → ((𝑓𝑢) ∈ 𝑧 ↔ (𝑓𝑢) ∈ 𝑢))
5452, 53bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑢 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝑢) ∈ 𝑢))
5550, 54imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑢 → ((𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢)))
5655rspccv 3579 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑢𝑥 → (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢)))
57 elneq 9535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤𝑧𝑤𝑧)
5857neneqd 2949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤𝑧 → ¬ 𝑤 = 𝑧)
59 vex 3450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑤 ∈ V
60 neqne 2952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑤 = 𝑧𝑤𝑧)
61 prel12g 4822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤𝑧) → ({𝑤, 𝑧} = {(𝑓𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓𝑢), 𝑢})))
6259, 23, 60, 61mp3an12i 1466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑤 = 𝑧 → ({𝑤, 𝑧} = {(𝑓𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓𝑢), 𝑢})))
63 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = {(𝑓𝑢), 𝑢} → (𝑤𝑣𝑤 ∈ {(𝑓𝑢), 𝑢}))
64 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = {(𝑓𝑢), 𝑢} → (𝑧𝑣𝑧 ∈ {(𝑓𝑢), 𝑢}))
6563, 64anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = {(𝑓𝑢), 𝑢} → ((𝑤𝑣𝑧𝑣) ↔ (𝑤 ∈ {(𝑓𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓𝑢), 𝑢})))
66 ancom 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑤𝑣𝑧𝑣) ↔ (𝑧𝑣𝑤𝑣))
6765, 66bitr3di 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 = {(𝑓𝑢), 𝑢} → ((𝑤 ∈ {(𝑓𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓𝑢), 𝑢}) ↔ (𝑧𝑣𝑤𝑣)))
6862, 67sylan9bbr 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 = {(𝑓𝑢), 𝑢} ∧ ¬ 𝑤 = 𝑧) → ({𝑤, 𝑧} = {(𝑓𝑢), 𝑢} ↔ (𝑧𝑣𝑤𝑣)))
6958, 68sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 = {(𝑓𝑢), 𝑢} ∧ 𝑤𝑧) → ({𝑤, 𝑧} = {(𝑓𝑢), 𝑢} ↔ (𝑧𝑣𝑤𝑣)))
7069adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 = {(𝑓𝑢), 𝑢} ∧ (𝑤𝑧 ∧ (𝑓𝑢) ∈ 𝑢)) → ({𝑤, 𝑧} = {(𝑓𝑢), 𝑢} ↔ (𝑧𝑣𝑤𝑣)))
7170pm5.32da 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = {(𝑓𝑢), 𝑢} → (((𝑤𝑧 ∧ (𝑓𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓𝑢), 𝑢}) ↔ ((𝑤𝑧 ∧ (𝑓𝑢) ∈ 𝑢) ∧ (𝑧𝑣𝑤𝑣))))
7223preleq 9553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑤𝑧 ∧ (𝑓𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓𝑢), 𝑢}) → (𝑤 = (𝑓𝑢) ∧ 𝑧 = 𝑢))
7371, 72syl6bir 254 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = {(𝑓𝑢), 𝑢} → (((𝑤𝑧 ∧ (𝑓𝑢) ∈ 𝑢) ∧ (𝑧𝑣𝑤𝑣)) → (𝑤 = (𝑓𝑢) ∧ 𝑧 = 𝑢)))
7451eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑢 → (𝑤 = (𝑓𝑧) ↔ 𝑤 = (𝑓𝑢)))
7574biimparc 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤 = (𝑓𝑢) ∧ 𝑧 = 𝑢) → 𝑤 = (𝑓𝑧))
7673, 75syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = {(𝑓𝑢), 𝑢} → (((𝑤𝑧 ∧ (𝑓𝑢) ∈ 𝑢) ∧ (𝑧𝑣𝑤𝑣)) → 𝑤 = (𝑓𝑧)))
7776exp4c 434 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = {(𝑓𝑢), 𝑢} → (𝑤𝑧 → ((𝑓𝑢) ∈ 𝑢 → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))))
7877com13 88 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑢) ∈ 𝑢 → (𝑤𝑧 → (𝑣 = {(𝑓𝑢), 𝑢} → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))))
7956, 78syl8 76 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑢𝑥 → (𝑢 ≠ ∅ → (𝑤𝑧 → (𝑣 = {(𝑓𝑢), 𝑢} → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))))))
8079com4r 94 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤𝑧 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑢𝑥 → (𝑢 ≠ ∅ → (𝑣 = {(𝑓𝑢), 𝑢} → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))))))
8180imp 408 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤𝑧 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) → (𝑢𝑥 → (𝑢 ≠ ∅ → (𝑣 = {(𝑓𝑢), 𝑢} → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧))))))
8281imp4a 424 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑧 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) → (𝑢𝑥 → ((𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢}) → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))))
8382com3l 89 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑥 → ((𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢}) → ((𝑤𝑧 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))))
8483rexlimiv 3146 . . . . . . . . . . . . . . . . . 18 (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢}) → ((𝑤𝑧 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧))))
8549, 84sylbi 216 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → ((𝑤𝑧 ∧ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)) → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧))))
8685expd 417 . . . . . . . . . . . . . . . 16 (𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → (𝑤𝑧 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))))
8786com13 88 . . . . . . . . . . . . . . 15 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑤𝑧 → (𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → ((𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))))
8887imp4b 423 . . . . . . . . . . . . . 14 ((∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ∧ 𝑤𝑧) → ((𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ∧ (𝑧𝑣𝑤𝑣)) → 𝑤 = (𝑓𝑧)))
8988exlimdv 1937 . . . . . . . . . . . . 13 ((∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ∧ 𝑤𝑧) → (∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ∧ (𝑧𝑣𝑤𝑣)) → 𝑤 = (𝑓𝑧)))
9044, 89biimtrid 241 . . . . . . . . . . . 12 ((∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ∧ 𝑤𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) → 𝑤 = (𝑓𝑧)))
9190expimpd 455 . . . . . . . . . . 11 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) → 𝑤 = (𝑓𝑧)))
9291alrimiv 1931 . . . . . . . . . 10 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∀𝑤((𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) → 𝑤 = (𝑓𝑧)))
93 mo2icl 3673 . . . . . . . . . 10 (∀𝑤((𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) → 𝑤 = (𝑓𝑧)) → ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
9492, 93syl 17 . . . . . . . . 9 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
9543, 94jctird 528 . . . . . . . 8 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑥𝑧 ≠ ∅) → (∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ∧ ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))))
96 df-reu 3355 . . . . . . . . 9 (∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) ↔ ∃!𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
97 df-eu 2568 . . . . . . . . 9 (∃!𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ↔ (∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ∧ ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
9896, 97bitri 275 . . . . . . . 8 (∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) ↔ (∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ∧ ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
9995, 98syl6ibr 252 . . . . . . 7 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑥𝑧 ≠ ∅) → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
10099expd 417 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑧𝑥 → (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
1012, 100ralrimi 3241 . . . . 5 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
102 vex 3450 . . . . . . . . . . 11 𝑓 ∈ V
103102rnex 7850 . . . . . . . . . 10 ran 𝑓 ∈ V
104 p0ex 5340 . . . . . . . . . 10 {∅} ∈ V
105103, 104unex 7681 . . . . . . . . 9 (ran 𝑓 ∪ {∅}) ∈ V
106 vex 3450 . . . . . . . . 9 𝑥 ∈ V
107105, 106unex 7681 . . . . . . . 8 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
108107pwex 5336 . . . . . . 7 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
109 ssun1 4133 . . . . . . . . . . . . . 14 (ran 𝑓 ∪ {∅}) ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
110 fvrn0 6873 . . . . . . . . . . . . . 14 (𝑓𝑢) ∈ (ran 𝑓 ∪ {∅})
111109, 110sselii 3942 . . . . . . . . . . . . 13 (𝑓𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
112 elun2 4138 . . . . . . . . . . . . 13 (𝑢𝑥𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
113 prssi 4782 . . . . . . . . . . . . 13 (((𝑓𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∧ 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) → {(𝑓𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
114111, 112, 113sylancr 588 . . . . . . . . . . . 12 (𝑢𝑥 → {(𝑓𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
115 prex 5390 . . . . . . . . . . . . 13 {(𝑓𝑢), 𝑢} ∈ V
116115elpw 4565 . . . . . . . . . . . 12 ({(𝑓𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
117114, 116sylibr 233 . . . . . . . . . . 11 (𝑢𝑥 → {(𝑓𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
118 eleq1 2826 . . . . . . . . . . 11 (𝑔 = {(𝑓𝑢), 𝑢} → (𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
119117, 118syl5ibrcom 247 . . . . . . . . . 10 (𝑢𝑥 → (𝑔 = {(𝑓𝑢), 𝑢} → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
120119adantld 492 . . . . . . . . 9 (𝑢𝑥 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
121120rexlimiv 3146 . . . . . . . 8 (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
122121abssi 4028 . . . . . . 7 {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ⊆ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
123108, 122ssexi 5280 . . . . . 6 {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ∈ V
124 rexeq 3311 . . . . . . . . 9 (𝑦 = {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → (∃𝑣𝑦 (𝑧𝑣𝑤𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
125124reubidv 3372 . . . . . . . 8 (𝑦 = {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → (∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣) ↔ ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
126125imbi2d 341 . . . . . . 7 (𝑦 = {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → ((𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)) ↔ (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
127126ralbidv 3175 . . . . . 6 (𝑦 = {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → (∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
128123, 127spcev 3566 . . . . 5 (∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
129101, 128syl 17 . . . 4 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
130129exlimiv 1934 . . 3 (∃𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
131130alimi 1814 . 2 (∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∀𝑥𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
1321, 131sylbi 216 1 (CHOICE → ∀𝑥𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wex 1782  wcel 2107  ∃*wmo 2537  ∃!weu 2567  {cab 2714  wne 2944  wral 3065  wrex 3074  ∃!wreu 3352  Vcvv 3446  cun 3909  wss 3911  c0 4283  𝒫 cpw 4561  {csn 4587  {cpr 4589  ran crn 5635  cfv 6497  CHOICEwac 10052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-reg 9529
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-eprel 5538  df-fr 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-fv 6505  df-ac 10053
This theorem is referenced by:  dfac2  10068
  Copyright terms: Public domain W3C validator