Metamath Proof Explorer


Theorem dfac2b

Description: Axiom of Choice (first form) of Enderton p. 49 implies our Axiom of Choice (in the form of ac3 ). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq and preleq 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 .) (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 16-Jun-2022)

Ref Expression
Assertion dfac2b ( CHOICE → ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )

Proof

Step Hyp Ref Expression
1 dfac3 ( CHOICE ↔ ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
2 nfra1 𝑧𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 )
3 rsp ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑧𝑥 → ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ) )
4 equid 𝑧 = 𝑧
5 neeq1 ( 𝑢 = 𝑧 → ( 𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅ ) )
6 eqeq1 ( 𝑢 = 𝑧 → ( 𝑢 = 𝑧𝑧 = 𝑧 ) )
7 5 6 anbi12d ( 𝑢 = 𝑧 → ( ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) ↔ ( 𝑧 ≠ ∅ ∧ 𝑧 = 𝑧 ) ) )
8 7 rspcev ( ( 𝑧𝑥 ∧ ( 𝑧 ≠ ∅ ∧ 𝑧 = 𝑧 ) ) → ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) )
9 4 8 mpanr2 ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) )
10 fveq2 ( 𝑢 = 𝑧 → ( 𝑓𝑢 ) = ( 𝑓𝑧 ) )
11 10 preq1d ( 𝑢 = 𝑧 → { ( 𝑓𝑢 ) , 𝑢 } = { ( 𝑓𝑧 ) , 𝑢 } )
12 preq2 ( 𝑢 = 𝑧 → { ( 𝑓𝑧 ) , 𝑢 } = { ( 𝑓𝑧 ) , 𝑧 } )
13 11 12 eqtr2d ( 𝑢 = 𝑧 → { ( 𝑓𝑧 ) , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } )
14 13 anim2i ( ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) → ( 𝑢 ≠ ∅ ∧ { ( 𝑓𝑧 ) , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) )
15 14 reximi ( ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) → ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ { ( 𝑓𝑧 ) , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) )
16 9 15 syl ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ { ( 𝑓𝑧 ) , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) )
17 prex { ( 𝑓𝑧 ) , 𝑧 } ∈ V
18 eqeq1 ( 𝑔 = { ( 𝑓𝑧 ) , 𝑧 } → ( 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ↔ { ( 𝑓𝑧 ) , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) )
19 18 anbi2d ( 𝑔 = { ( 𝑓𝑧 ) , 𝑧 } → ( ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) ↔ ( 𝑢 ≠ ∅ ∧ { ( 𝑓𝑧 ) , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) ) )
20 19 rexbidv ( 𝑔 = { ( 𝑓𝑧 ) , 𝑧 } → ( ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) ↔ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ { ( 𝑓𝑧 ) , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) ) )
21 17 20 elab ( { ( 𝑓𝑧 ) , 𝑧 } ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ↔ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ { ( 𝑓𝑧 ) , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) )
22 16 21 sylibr ( ( 𝑧𝑥𝑧 ≠ ∅ ) → { ( 𝑓𝑧 ) , 𝑧 } ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } )
23 vex 𝑧 ∈ V
24 23 prid2 𝑧 ∈ { ( 𝑓𝑧 ) , 𝑧 }
25 fvex ( 𝑓𝑧 ) ∈ V
26 25 prid1 ( 𝑓𝑧 ) ∈ { ( 𝑓𝑧 ) , 𝑧 }
27 24 26 pm3.2i ( 𝑧 ∈ { ( 𝑓𝑧 ) , 𝑧 } ∧ ( 𝑓𝑧 ) ∈ { ( 𝑓𝑧 ) , 𝑧 } )
28 eleq2 ( 𝑣 = { ( 𝑓𝑧 ) , 𝑧 } → ( 𝑧𝑣𝑧 ∈ { ( 𝑓𝑧 ) , 𝑧 } ) )
29 eleq2 ( 𝑣 = { ( 𝑓𝑧 ) , 𝑧 } → ( ( 𝑓𝑧 ) ∈ 𝑣 ↔ ( 𝑓𝑧 ) ∈ { ( 𝑓𝑧 ) , 𝑧 } ) )
30 28 29 anbi12d ( 𝑣 = { ( 𝑓𝑧 ) , 𝑧 } → ( ( 𝑧𝑣 ∧ ( 𝑓𝑧 ) ∈ 𝑣 ) ↔ ( 𝑧 ∈ { ( 𝑓𝑧 ) , 𝑧 } ∧ ( 𝑓𝑧 ) ∈ { ( 𝑓𝑧 ) , 𝑧 } ) ) )
31 30 rspcev ( ( { ( 𝑓𝑧 ) , 𝑧 } ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ∧ ( 𝑧 ∈ { ( 𝑓𝑧 ) , 𝑧 } ∧ ( 𝑓𝑧 ) ∈ { ( 𝑓𝑧 ) , 𝑧 } ) ) → ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣 ∧ ( 𝑓𝑧 ) ∈ 𝑣 ) )
32 22 27 31 sylancl ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣 ∧ ( 𝑓𝑧 ) ∈ 𝑣 ) )
33 eleq1 ( 𝑤 = ( 𝑓𝑧 ) → ( 𝑤𝑧 ↔ ( 𝑓𝑧 ) ∈ 𝑧 ) )
34 eleq1 ( 𝑤 = ( 𝑓𝑧 ) → ( 𝑤𝑣 ↔ ( 𝑓𝑧 ) ∈ 𝑣 ) )
35 34 anbi2d ( 𝑤 = ( 𝑓𝑧 ) → ( ( 𝑧𝑣𝑤𝑣 ) ↔ ( 𝑧𝑣 ∧ ( 𝑓𝑧 ) ∈ 𝑣 ) ) )
36 35 rexbidv ( 𝑤 = ( 𝑓𝑧 ) → ( ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ↔ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣 ∧ ( 𝑓𝑧 ) ∈ 𝑣 ) ) )
37 33 36 anbi12d ( 𝑤 = ( 𝑓𝑧 ) → ( ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ↔ ( ( 𝑓𝑧 ) ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣 ∧ ( 𝑓𝑧 ) ∈ 𝑣 ) ) ) )
38 25 37 spcev ( ( ( 𝑓𝑧 ) ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣 ∧ ( 𝑓𝑧 ) ∈ 𝑣 ) ) → ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
39 32 38 sylan2 ( ( ( 𝑓𝑧 ) ∈ 𝑧 ∧ ( 𝑧𝑥𝑧 ≠ ∅ ) ) → ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
40 39 ex ( ( 𝑓𝑧 ) ∈ 𝑧 → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) )
41 3 40 syl8 ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑧𝑥 → ( 𝑧 ≠ ∅ → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) ) ) )
42 41 impd ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) ) )
43 42 pm2.43d ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) )
44 df-rex ( ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ↔ ∃ 𝑣 ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ∧ ( 𝑧𝑣𝑤𝑣 ) ) )
45 vex 𝑣 ∈ V
46 eqeq1 ( 𝑔 = 𝑣 → ( 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ↔ 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ) )
47 46 anbi2d ( 𝑔 = 𝑣 → ( ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) ↔ ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ) ) )
48 47 rexbidv ( 𝑔 = 𝑣 → ( ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) ↔ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ) ) )
49 45 48 elab ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ↔ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ) )
50 neeq1 ( 𝑧 = 𝑢 → ( 𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅ ) )
51 fveq2 ( 𝑧 = 𝑢 → ( 𝑓𝑧 ) = ( 𝑓𝑢 ) )
52 51 eleq1d ( 𝑧 = 𝑢 → ( ( 𝑓𝑧 ) ∈ 𝑧 ↔ ( 𝑓𝑢 ) ∈ 𝑧 ) )
53 eleq2 ( 𝑧 = 𝑢 → ( ( 𝑓𝑢 ) ∈ 𝑧 ↔ ( 𝑓𝑢 ) ∈ 𝑢 ) )
54 52 53 bitrd ( 𝑧 = 𝑢 → ( ( 𝑓𝑧 ) ∈ 𝑧 ↔ ( 𝑓𝑢 ) ∈ 𝑢 ) )
55 50 54 imbi12d ( 𝑧 = 𝑢 → ( ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ↔ ( 𝑢 ≠ ∅ → ( 𝑓𝑢 ) ∈ 𝑢 ) ) )
56 55 rspccv ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑢𝑥 → ( 𝑢 ≠ ∅ → ( 𝑓𝑢 ) ∈ 𝑢 ) ) )
57 elneq ( 𝑤𝑧𝑤𝑧 )
58 57 neneqd ( 𝑤𝑧 → ¬ 𝑤 = 𝑧 )
59 vex 𝑤 ∈ V
60 neqne ( ¬ 𝑤 = 𝑧𝑤𝑧 )
61 prel12g ( ( 𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤𝑧 ) → ( { 𝑤 , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ↔ ( 𝑤 ∈ { ( 𝑓𝑢 ) , 𝑢 } ∧ 𝑧 ∈ { ( 𝑓𝑢 ) , 𝑢 } ) ) )
62 59 23 60 61 mp3an12i ( ¬ 𝑤 = 𝑧 → ( { 𝑤 , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ↔ ( 𝑤 ∈ { ( 𝑓𝑢 ) , 𝑢 } ∧ 𝑧 ∈ { ( 𝑓𝑢 ) , 𝑢 } ) ) )
63 eleq2 ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( 𝑤𝑣𝑤 ∈ { ( 𝑓𝑢 ) , 𝑢 } ) )
64 eleq2 ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( 𝑧𝑣𝑧 ∈ { ( 𝑓𝑢 ) , 𝑢 } ) )
65 63 64 anbi12d ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( 𝑤𝑣𝑧𝑣 ) ↔ ( 𝑤 ∈ { ( 𝑓𝑢 ) , 𝑢 } ∧ 𝑧 ∈ { ( 𝑓𝑢 ) , 𝑢 } ) ) )
66 ancom ( ( 𝑤𝑣𝑧𝑣 ) ↔ ( 𝑧𝑣𝑤𝑣 ) )
67 65 66 bitr3di ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( 𝑤 ∈ { ( 𝑓𝑢 ) , 𝑢 } ∧ 𝑧 ∈ { ( 𝑓𝑢 ) , 𝑢 } ) ↔ ( 𝑧𝑣𝑤𝑣 ) ) )
68 62 67 sylan9bbr ( ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ∧ ¬ 𝑤 = 𝑧 ) → ( { 𝑤 , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ↔ ( 𝑧𝑣𝑤𝑣 ) ) )
69 58 68 sylan2 ( ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ∧ 𝑤𝑧 ) → ( { 𝑤 , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ↔ ( 𝑧𝑣𝑤𝑣 ) ) )
70 69 adantrr ( ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ∧ ( 𝑤𝑧 ∧ ( 𝑓𝑢 ) ∈ 𝑢 ) ) → ( { 𝑤 , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ↔ ( 𝑧𝑣𝑤𝑣 ) ) )
71 70 pm5.32da ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( ( 𝑤𝑧 ∧ ( 𝑓𝑢 ) ∈ 𝑢 ) ∧ { 𝑤 , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) ↔ ( ( 𝑤𝑧 ∧ ( 𝑓𝑢 ) ∈ 𝑢 ) ∧ ( 𝑧𝑣𝑤𝑣 ) ) ) )
72 23 preleq ( ( ( 𝑤𝑧 ∧ ( 𝑓𝑢 ) ∈ 𝑢 ) ∧ { 𝑤 , 𝑧 } = { ( 𝑓𝑢 ) , 𝑢 } ) → ( 𝑤 = ( 𝑓𝑢 ) ∧ 𝑧 = 𝑢 ) )
73 71 72 syl6bir ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( ( 𝑤𝑧 ∧ ( 𝑓𝑢 ) ∈ 𝑢 ) ∧ ( 𝑧𝑣𝑤𝑣 ) ) → ( 𝑤 = ( 𝑓𝑢 ) ∧ 𝑧 = 𝑢 ) ) )
74 51 eqeq2d ( 𝑧 = 𝑢 → ( 𝑤 = ( 𝑓𝑧 ) ↔ 𝑤 = ( 𝑓𝑢 ) ) )
75 74 biimparc ( ( 𝑤 = ( 𝑓𝑢 ) ∧ 𝑧 = 𝑢 ) → 𝑤 = ( 𝑓𝑧 ) )
76 73 75 syl6 ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( ( 𝑤𝑧 ∧ ( 𝑓𝑢 ) ∈ 𝑢 ) ∧ ( 𝑧𝑣𝑤𝑣 ) ) → 𝑤 = ( 𝑓𝑧 ) ) )
77 76 exp4c ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( 𝑤𝑧 → ( ( 𝑓𝑢 ) ∈ 𝑢 → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) )
78 77 com13 ( ( 𝑓𝑢 ) ∈ 𝑢 → ( 𝑤𝑧 → ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) )
79 56 78 syl8 ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑢𝑥 → ( 𝑢 ≠ ∅ → ( 𝑤𝑧 → ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) ) ) )
80 79 com4r ( 𝑤𝑧 → ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑢𝑥 → ( 𝑢 ≠ ∅ → ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) ) ) )
81 80 imp ( ( 𝑤𝑧 ∧ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ) → ( 𝑢𝑥 → ( 𝑢 ≠ ∅ → ( 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) ) )
82 81 imp4a ( ( 𝑤𝑧 ∧ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ) → ( 𝑢𝑥 → ( ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ) → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) )
83 82 com3l ( 𝑢𝑥 → ( ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ) → ( ( 𝑤𝑧 ∧ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ) → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) )
84 83 rexlimiv ( ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓𝑢 ) , 𝑢 } ) → ( ( 𝑤𝑧 ∧ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ) → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) )
85 49 84 sylbi ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } → ( ( 𝑤𝑧 ∧ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ) → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) )
86 85 expd ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } → ( 𝑤𝑧 → ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) )
87 86 com13 ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑤𝑧 → ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } → ( ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) ) ) )
88 87 imp4b ( ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑤𝑧 ) → ( ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ∧ ( 𝑧𝑣𝑤𝑣 ) ) → 𝑤 = ( 𝑓𝑧 ) ) )
89 88 exlimdv ( ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑤𝑧 ) → ( ∃ 𝑣 ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ∧ ( 𝑧𝑣𝑤𝑣 ) ) → 𝑤 = ( 𝑓𝑧 ) ) )
90 44 89 syl5bi ( ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑤𝑧 ) → ( ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) → 𝑤 = ( 𝑓𝑧 ) ) )
91 90 expimpd ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) → 𝑤 = ( 𝑓𝑧 ) ) )
92 91 alrimiv ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) → 𝑤 = ( 𝑓𝑧 ) ) )
93 mo2icl ( ∀ 𝑤 ( ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) → 𝑤 = ( 𝑓𝑧 ) ) → ∃* 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
94 92 93 syl ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ∃* 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
95 43 94 jctird ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ( ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ∧ ∃* 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) ) )
96 df-reu ( ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ↔ ∃! 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
97 df-eu ( ∃! 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ↔ ( ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ∧ ∃* 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) )
98 96 97 bitri ( ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ↔ ( ∃ 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ∧ ∃* 𝑤 ( 𝑤𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) )
99 95 98 syl6ibr ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
100 99 expd ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑧𝑥 → ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) )
101 2 100 ralrimi ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
102 vex 𝑓 ∈ V
103 102 rnex ran 𝑓 ∈ V
104 p0ex { ∅ } ∈ V
105 103 104 unex ( ran 𝑓 ∪ { ∅ } ) ∈ V
106 vex 𝑥 ∈ V
107 105 106 unex ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ∈ V
108 107 pwex 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ∈ V
109 ssun1 ( ran 𝑓 ∪ { ∅ } ) ⊆ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 )
110 fvrn0 ( 𝑓𝑢 ) ∈ ( ran 𝑓 ∪ { ∅ } )
111 109 110 sselii ( 𝑓𝑢 ) ∈ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 )
112 elun2 ( 𝑢𝑥𝑢 ∈ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
113 prssi ( ( ( 𝑓𝑢 ) ∈ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ∧ 𝑢 ∈ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ) → { ( 𝑓𝑢 ) , 𝑢 } ⊆ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
114 111 112 113 sylancr ( 𝑢𝑥 → { ( 𝑓𝑢 ) , 𝑢 } ⊆ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
115 prex { ( 𝑓𝑢 ) , 𝑢 } ∈ V
116 115 elpw ( { ( 𝑓𝑢 ) , 𝑢 } ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ↔ { ( 𝑓𝑢 ) , 𝑢 } ⊆ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
117 114 116 sylibr ( 𝑢𝑥 → { ( 𝑓𝑢 ) , 𝑢 } ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
118 eleq1 ( 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } → ( 𝑔 ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ↔ { ( 𝑓𝑢 ) , 𝑢 } ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ) )
119 117 118 syl5ibrcom ( 𝑢𝑥 → ( 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } → 𝑔 ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ) )
120 119 adantld ( 𝑢𝑥 → ( ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) → 𝑔 ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ) )
121 120 rexlimiv ( ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) → 𝑔 ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
122 121 abssi { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ⊆ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 )
123 108 122 ssexi { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ∈ V
124 rexeq ( 𝑦 = { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } → ( ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ↔ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
125 124 reubidv ( 𝑦 = { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } → ( ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ↔ ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) )
126 125 imbi2d ( 𝑦 = { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } → ( ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) )
127 126 ralbidv ( 𝑦 = { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } → ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) ↔ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) ) )
128 123 127 spcev ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣 ∈ { 𝑔 ∣ ∃ 𝑢𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓𝑢 ) , 𝑢 } ) } ( 𝑧𝑣𝑤𝑣 ) ) → ∃ 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
129 101 128 syl ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ∃ 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
130 129 exlimiv ( ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ∃ 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
131 130 alimi ( ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
132 1 131 sylbi ( CHOICE → ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )