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

Theorem dfac2b 10125
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies our Axiom of Choice (in the form of ac3 10457). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq 9593 and preleq 9611 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 10124.) (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 10116 . 2 (CHOICE ↔ ∀𝑥𝑓𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧))
2 nfra1 3282 . . . . . 6 𝑧𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)
3 rsp 3245 . . . . . . . . . . . 12 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑧𝑥 → (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧)))
4 equid 2016 . . . . . . . . . . . . . . . . . 18 𝑧 = 𝑧
5 neeq1 3004 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
6 eqeq1 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑧 → (𝑢 = 𝑧𝑧 = 𝑧))
75, 6anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) ↔ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)))
87rspcev 3613 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑥 ∧ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)) → ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
94, 8mpanr2 703 . . . . . . . . . . . . . . . . 17 ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧))
10 fveq2 6892 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑧 → (𝑓𝑢) = (𝑓𝑧))
1110preq1d 4744 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑧 → {(𝑓𝑢), 𝑢} = {(𝑓𝑧), 𝑢})
12 preq2 4739 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑧 → {(𝑓𝑧), 𝑢} = {(𝑓𝑧), 𝑧})
1311, 12eqtr2d 2774 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑧 → {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢})
1413anim2i 618 . . . . . . . . . . . . . . . . . 18 ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
1514reximi 3085 . . . . . . . . . . . . . . . . 17 (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
169, 15syl 17 . . . . . . . . . . . . . . . 16 ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
17 prex 5433 . . . . . . . . . . . . . . . . 17 {(𝑓𝑧), 𝑧} ∈ V
18 eqeq1 2737 . . . . . . . . . . . . . . . . . . 19 (𝑔 = {(𝑓𝑧), 𝑧} → (𝑔 = {(𝑓𝑢), 𝑢} ↔ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
1918anbi2d 630 . . . . . . . . . . . . . . . . . 18 (𝑔 = {(𝑓𝑧), 𝑧} → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢})))
2019rexbidv 3179 . . . . . . . . . . . . . . . . 17 (𝑔 = {(𝑓𝑧), 𝑧} → (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) ↔ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢})))
2117, 20elab 3669 . . . . . . . . . . . . . . . 16 ({(𝑓𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ↔ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ {(𝑓𝑧), 𝑧} = {(𝑓𝑢), 𝑢}))
2216, 21sylibr 233 . . . . . . . . . . . . . . 15 ((𝑧𝑥𝑧 ≠ ∅) → {(𝑓𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})})
23 vex 3479 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
2423prid2 4768 . . . . . . . . . . . . . . . 16 𝑧 ∈ {(𝑓𝑧), 𝑧}
25 fvex 6905 . . . . . . . . . . . . . . . . 17 (𝑓𝑧) ∈ V
2625prid1 4767 . . . . . . . . . . . . . . . 16 (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧}
2724, 26pm3.2i 472 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑓𝑧), 𝑧} ∧ (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧})
28 eleq2 2823 . . . . . . . . . . . . . . . . 17 (𝑣 = {(𝑓𝑧), 𝑧} → (𝑧𝑣𝑧 ∈ {(𝑓𝑧), 𝑧}))
29 eleq2 2823 . . . . . . . . . . . . . . . . 17 (𝑣 = {(𝑓𝑧), 𝑧} → ((𝑓𝑧) ∈ 𝑣 ↔ (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧}))
3028, 29anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑣 = {(𝑓𝑧), 𝑧} → ((𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣) ↔ (𝑧 ∈ {(𝑓𝑧), 𝑧} ∧ (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧})))
3130rspcev 3613 . . . . . . . . . . . . . . 15 (({(𝑓𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ∧ (𝑧 ∈ {(𝑓𝑧), 𝑧} ∧ (𝑓𝑧) ∈ {(𝑓𝑧), 𝑧})) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣))
3222, 27, 31sylancl 587 . . . . . . . . . . . . . 14 ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣))
33 eleq1 2822 . . . . . . . . . . . . . . . 16 (𝑤 = (𝑓𝑧) → (𝑤𝑧 ↔ (𝑓𝑧) ∈ 𝑧))
34 eleq1 2822 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝑓𝑧) → (𝑤𝑣 ↔ (𝑓𝑧) ∈ 𝑣))
3534anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝑓𝑧) → ((𝑧𝑣𝑤𝑣) ↔ (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣)))
3635rexbidv 3179 . . . . . . . . . . . . . . . 16 (𝑤 = (𝑓𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣)))
3733, 36anbi12d 632 . . . . . . . . . . . . . . 15 (𝑤 = (𝑓𝑧) → ((𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ↔ ((𝑓𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣))))
3825, 37spcev 3597 . . . . . . . . . . . . . 14 (((𝑓𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣 ∧ (𝑓𝑧) ∈ 𝑣)) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
3932, 38sylan2 594 . . . . . . . . . . . . 13 (((𝑓𝑧) ∈ 𝑧 ∧ (𝑧𝑥𝑧 ≠ ∅)) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
4039ex 414 . . . . . . . . . . . 12 ((𝑓𝑧) ∈ 𝑧 → ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
413, 40syl8 76 . . . . . . . . . . 11 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑧𝑥 → (𝑧 ≠ ∅ → ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))))
4241impd 412 . . . . . . . . . 10 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑥𝑧 ≠ ∅) → ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))))
4342pm2.43d 53 . . . . . . . . 9 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑥𝑧 ≠ ∅) → ∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
44 df-rex 3072 . . . . . . . . . . . . 13 (∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) ↔ ∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ∧ (𝑧𝑣𝑤𝑣)))
45 vex 3479 . . . . . . . . . . . . . . . . . . 19 𝑣 ∈ V
46 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑣 → (𝑔 = {(𝑓𝑢), 𝑢} ↔ 𝑣 = {(𝑓𝑢), 𝑢}))
4746anbi2d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑣 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢})))
4847rexbidv 3179 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑣 → (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) ↔ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢})))
4945, 48elab 3669 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ↔ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓𝑢), 𝑢}))
50 neeq1 3004 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑢 → (𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅))
51 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑢 → (𝑓𝑧) = (𝑓𝑢))
5251eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑢 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝑢) ∈ 𝑧))
53 eleq2 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑢 → ((𝑓𝑢) ∈ 𝑧 ↔ (𝑓𝑢) ∈ 𝑢))
5452, 53bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑢 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝑢) ∈ 𝑢))
5550, 54imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑢 → ((𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) ↔ (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢)))
5655rspccv 3610 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑢𝑥 → (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢)))
57 elneq 9593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤𝑧𝑤𝑧)
5857neneqd 2946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤𝑧 → ¬ 𝑤 = 𝑧)
59 vex 3479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑤 ∈ V
60 neqne 2949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑤 = 𝑧𝑤𝑧)
61 prel12g 4865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤𝑧) → ({𝑤, 𝑧} = {(𝑓𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓𝑢), 𝑢})))
6259, 23, 60, 61mp3an12i 1466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑤 = 𝑧 → ({𝑤, 𝑧} = {(𝑓𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓𝑢), 𝑢})))
63 eleq2 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = {(𝑓𝑢), 𝑢} → (𝑤𝑣𝑤 ∈ {(𝑓𝑢), 𝑢}))
64 eleq2 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9611 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑤𝑧 ∧ (𝑓𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓𝑢), 𝑢}) → (𝑤 = (𝑓𝑢) ∧ 𝑧 = 𝑢))
7371, 72syl6bir 254 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = {(𝑓𝑢), 𝑢} → (((𝑤𝑧 ∧ (𝑓𝑢) ∈ 𝑢) ∧ (𝑧𝑣𝑤𝑣)) → (𝑤 = (𝑓𝑢) ∧ 𝑧 = 𝑢)))
7451eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3149 . . . . . . . . . . . . . . . . . 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 3711 . . . . . . . . . 10 (∀𝑤((𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) → 𝑤 = (𝑓𝑧)) → ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
9492, 93syl 17 . . . . . . . . 9 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
9543, 94jctird 528 . . . . . . . 8 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑥𝑧 ≠ ∅) → (∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ∧ ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))))
96 df-reu 3378 . . . . . . . . 9 (∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) ↔ ∃!𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
97 df-eu 2564 . . . . . . . . 9 (∃!𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ↔ (∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ∧ ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
9896, 97bitri 275 . . . . . . . 8 (∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣) ↔ (∃𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)) ∧ ∃*𝑤(𝑤𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
9995, 98imbitrrdi 251 . . . . . . 7 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ((𝑧𝑥𝑧 ≠ ∅) → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
10099expd 417 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → (𝑧𝑥 → (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
1012, 100ralrimi 3255 . . . . 5 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑓𝑧) ∈ 𝑧) → ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
102 vex 3479 . . . . . . . . . . 11 𝑓 ∈ V
103102rnex 7903 . . . . . . . . . 10 ran 𝑓 ∈ V
104 p0ex 5383 . . . . . . . . . 10 {∅} ∈ V
105103, 104unex 7733 . . . . . . . . 9 (ran 𝑓 ∪ {∅}) ∈ V
106 vex 3479 . . . . . . . . 9 𝑥 ∈ V
107105, 106unex 7733 . . . . . . . 8 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
108107pwex 5379 . . . . . . 7 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∈ V
109 ssun1 4173 . . . . . . . . . . . . . 14 (ran 𝑓 ∪ {∅}) ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
110 fvrn0 6922 . . . . . . . . . . . . . 14 (𝑓𝑢) ∈ (ran 𝑓 ∪ {∅})
111109, 110sselii 3980 . . . . . . . . . . . . 13 (𝑓𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
112 elun2 4178 . . . . . . . . . . . . 13 (𝑢𝑥𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
113 prssi 4825 . . . . . . . . . . . . 13 (((𝑓𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∧ 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) → {(𝑓𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
114111, 112, 113sylancr 588 . . . . . . . . . . . 12 (𝑢𝑥 → {(𝑓𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
115 prex 5433 . . . . . . . . . . . . 13 {(𝑓𝑢), 𝑢} ∈ V
116115elpw 4607 . . . . . . . . . . . 12 ({(𝑓𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
117114, 116sylibr 233 . . . . . . . . . . 11 (𝑢𝑥 → {(𝑓𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
118 eleq1 2822 . . . . . . . . . . 11 (𝑔 = {(𝑓𝑢), 𝑢} → (𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
119117, 118syl5ibrcom 246 . . . . . . . . . 10 (𝑢𝑥 → (𝑔 = {(𝑓𝑢), 𝑢} → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
120119adantld 492 . . . . . . . . 9 (𝑢𝑥 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)))
121120rexlimiv 3149 . . . . . . . 8 (∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))
122121abssi 4068 . . . . . . 7 {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ⊆ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)
123108, 122ssexi 5323 . . . . . 6 {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} ∈ V
124 rexeq 3322 . . . . . . . . 9 (𝑦 = {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → (∃𝑣𝑦 (𝑧𝑣𝑤𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
125124reubidv 3395 . . . . . . . 8 (𝑦 = {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → (∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣) ↔ ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣)))
126125imbi2d 341 . . . . . . 7 (𝑦 = {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → ((𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)) ↔ (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
127126ralbidv 3178 . . . . . 6 (𝑦 = {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} → (∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣 ∈ {𝑔 ∣ ∃𝑢𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓𝑢), 𝑢})} (𝑧𝑣𝑤𝑣))))
128123, 127spcev 3597 . . . . 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 2533  ∃!weu 2563  {cab 2710  wne 2941  wral 3062  wrex 3071  ∃!wreu 3375  Vcvv 3475  cun 3947  wss 3949  c0 4323  𝒫 cpw 4603  {csn 4629  {cpr 4631  ran crn 5678  cfv 6544  CHOICEwac 10110
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 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-reg 9587
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-eprel 5581  df-fr 5632  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-fv 6552  df-ac 10111
This theorem is referenced by:  dfac2  10126
  Copyright terms: Public domain W3C validator