Metamath Proof Explorer


Theorem dfac5

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)

Ref Expression
Assertion dfac5 ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 dfac4 ( CHOICE ↔ ∀ 𝑥𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ) )
2 neeq1 ( 𝑧 = 𝑤 → ( 𝑧 ≠ ∅ ↔ 𝑤 ≠ ∅ ) )
3 2 cbvralvw ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ↔ ∀ 𝑤𝑥 𝑤 ≠ ∅ )
4 3 anbi2i ( ( ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ ∀ 𝑧𝑥 𝑧 ≠ ∅ ) ↔ ( ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ ∀ 𝑤𝑥 𝑤 ≠ ∅ ) )
5 r19.26 ( ∀ 𝑤𝑥 ( ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑤 ≠ ∅ ) ↔ ( ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ ∀ 𝑤𝑥 𝑤 ≠ ∅ ) )
6 4 5 bitr4i ( ( ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ ∀ 𝑧𝑥 𝑧 ≠ ∅ ) ↔ ∀ 𝑤𝑥 ( ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑤 ≠ ∅ ) )
7 pm3.35 ( ( 𝑤 ≠ ∅ ∧ ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ) → ( 𝑓𝑤 ) ∈ 𝑤 )
8 7 ancoms ( ( ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑤 ≠ ∅ ) → ( 𝑓𝑤 ) ∈ 𝑤 )
9 8 ralimi ( ∀ 𝑤𝑥 ( ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑤 ≠ ∅ ) → ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 )
10 6 9 sylbi ( ( ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ ∀ 𝑧𝑥 𝑧 ≠ ∅ ) → ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 )
11 r19.26 ( ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) ↔ ( ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ∧ ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) )
12 elin ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ ( 𝑣𝑧𝑣 ∈ ran 𝑓 ) )
13 fvelrnb ( 𝑓 Fn 𝑥 → ( 𝑣 ∈ ran 𝑓 ↔ ∃ 𝑡𝑥 ( 𝑓𝑡 ) = 𝑣 ) )
14 13 biimpac ( ( 𝑣 ∈ ran 𝑓𝑓 Fn 𝑥 ) → ∃ 𝑡𝑥 ( 𝑓𝑡 ) = 𝑣 )
15 fveq2 ( 𝑤 = 𝑡 → ( 𝑓𝑤 ) = ( 𝑓𝑡 ) )
16 id ( 𝑤 = 𝑡𝑤 = 𝑡 )
17 15 16 eleq12d ( 𝑤 = 𝑡 → ( ( 𝑓𝑤 ) ∈ 𝑤 ↔ ( 𝑓𝑡 ) ∈ 𝑡 ) )
18 neeq2 ( 𝑤 = 𝑡 → ( 𝑧𝑤𝑧𝑡 ) )
19 ineq2 ( 𝑤 = 𝑡 → ( 𝑧𝑤 ) = ( 𝑧𝑡 ) )
20 19 eqeq1d ( 𝑤 = 𝑡 → ( ( 𝑧𝑤 ) = ∅ ↔ ( 𝑧𝑡 ) = ∅ ) )
21 18 20 imbi12d ( 𝑤 = 𝑡 → ( ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ↔ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) )
22 17 21 anbi12d ( 𝑤 = 𝑡 → ( ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) ↔ ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) ) )
23 22 rspcv ( 𝑡𝑥 → ( ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) ) )
24 minel ( ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 ) = ∅ ) → ¬ ( 𝑓𝑡 ) ∈ 𝑧 )
25 24 ex ( ( 𝑓𝑡 ) ∈ 𝑡 → ( ( 𝑧𝑡 ) = ∅ → ¬ ( 𝑓𝑡 ) ∈ 𝑧 ) )
26 25 imim2d ( ( 𝑓𝑡 ) ∈ 𝑡 → ( ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) → ( 𝑧𝑡 → ¬ ( 𝑓𝑡 ) ∈ 𝑧 ) ) )
27 26 imp ( ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) → ( 𝑧𝑡 → ¬ ( 𝑓𝑡 ) ∈ 𝑧 ) )
28 27 necon4ad ( ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) → ( ( 𝑓𝑡 ) ∈ 𝑧𝑧 = 𝑡 ) )
29 eleq1 ( ( 𝑓𝑡 ) = 𝑣 → ( ( 𝑓𝑡 ) ∈ 𝑧𝑣𝑧 ) )
30 29 biimpar ( ( ( 𝑓𝑡 ) = 𝑣𝑣𝑧 ) → ( 𝑓𝑡 ) ∈ 𝑧 )
31 28 30 impel ( ( ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) ∧ ( ( 𝑓𝑡 ) = 𝑣𝑣𝑧 ) ) → 𝑧 = 𝑡 )
32 fveq2 ( 𝑧 = 𝑡 → ( 𝑓𝑧 ) = ( 𝑓𝑡 ) )
33 eqeq2 ( ( 𝑓𝑡 ) = 𝑣 → ( ( 𝑓𝑧 ) = ( 𝑓𝑡 ) ↔ ( 𝑓𝑧 ) = 𝑣 ) )
34 eqcom ( ( 𝑓𝑧 ) = 𝑣𝑣 = ( 𝑓𝑧 ) )
35 33 34 bitrdi ( ( 𝑓𝑡 ) = 𝑣 → ( ( 𝑓𝑧 ) = ( 𝑓𝑡 ) ↔ 𝑣 = ( 𝑓𝑧 ) ) )
36 32 35 syl5ib ( ( 𝑓𝑡 ) = 𝑣 → ( 𝑧 = 𝑡𝑣 = ( 𝑓𝑧 ) ) )
37 36 ad2antrl ( ( ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) ∧ ( ( 𝑓𝑡 ) = 𝑣𝑣𝑧 ) ) → ( 𝑧 = 𝑡𝑣 = ( 𝑓𝑧 ) ) )
38 31 37 mpd ( ( ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) ∧ ( ( 𝑓𝑡 ) = 𝑣𝑣𝑧 ) ) → 𝑣 = ( 𝑓𝑧 ) )
39 38 exp32 ( ( ( 𝑓𝑡 ) ∈ 𝑡 ∧ ( 𝑧𝑡 → ( 𝑧𝑡 ) = ∅ ) ) → ( ( 𝑓𝑡 ) = 𝑣 → ( 𝑣𝑧𝑣 = ( 𝑓𝑧 ) ) ) )
40 23 39 syl6com ( ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ( 𝑡𝑥 → ( ( 𝑓𝑡 ) = 𝑣 → ( 𝑣𝑧𝑣 = ( 𝑓𝑧 ) ) ) ) )
41 40 com14 ( 𝑣𝑧 → ( 𝑡𝑥 → ( ( 𝑓𝑡 ) = 𝑣 → ( ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → 𝑣 = ( 𝑓𝑧 ) ) ) ) )
42 41 rexlimdv ( 𝑣𝑧 → ( ∃ 𝑡𝑥 ( 𝑓𝑡 ) = 𝑣 → ( ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → 𝑣 = ( 𝑓𝑧 ) ) ) )
43 14 42 syl5 ( 𝑣𝑧 → ( ( 𝑣 ∈ ran 𝑓𝑓 Fn 𝑥 ) → ( ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → 𝑣 = ( 𝑓𝑧 ) ) ) )
44 43 expd ( 𝑣𝑧 → ( 𝑣 ∈ ran 𝑓 → ( 𝑓 Fn 𝑥 → ( ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → 𝑣 = ( 𝑓𝑧 ) ) ) ) )
45 44 com4t ( 𝑓 Fn 𝑥 → ( ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ( 𝑣𝑧 → ( 𝑣 ∈ ran 𝑓𝑣 = ( 𝑓𝑧 ) ) ) ) )
46 45 imp4b ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) ) → ( ( 𝑣𝑧𝑣 ∈ ran 𝑓 ) → 𝑣 = ( 𝑓𝑧 ) ) )
47 12 46 syl5bi ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( ( 𝑓𝑤 ) ∈ 𝑤 ∧ ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) ) → ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) → 𝑣 = ( 𝑓𝑧 ) ) )
48 11 47 sylan2br ( ( 𝑓 Fn 𝑥 ∧ ( ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ∧ ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) ) → ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) → 𝑣 = ( 𝑓𝑧 ) ) )
49 48 anassrs ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) → 𝑣 = ( 𝑓𝑧 ) ) )
50 49 adantlr ( ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑧𝑥 ) ∧ ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) → 𝑣 = ( 𝑓𝑧 ) ) )
51 fveq2 ( 𝑤 = 𝑧 → ( 𝑓𝑤 ) = ( 𝑓𝑧 ) )
52 id ( 𝑤 = 𝑧𝑤 = 𝑧 )
53 51 52 eleq12d ( 𝑤 = 𝑧 → ( ( 𝑓𝑤 ) ∈ 𝑤 ↔ ( 𝑓𝑧 ) ∈ 𝑧 ) )
54 53 rspcv ( 𝑧𝑥 → ( ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 → ( 𝑓𝑧 ) ∈ 𝑧 ) )
55 fnfvelrn ( ( 𝑓 Fn 𝑥𝑧𝑥 ) → ( 𝑓𝑧 ) ∈ ran 𝑓 )
56 55 expcom ( 𝑧𝑥 → ( 𝑓 Fn 𝑥 → ( 𝑓𝑧 ) ∈ ran 𝑓 ) )
57 54 56 anim12d ( 𝑧𝑥 → ( ( ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤𝑓 Fn 𝑥 ) → ( ( 𝑓𝑧 ) ∈ 𝑧 ∧ ( 𝑓𝑧 ) ∈ ran 𝑓 ) ) )
58 elin ( ( 𝑓𝑧 ) ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ ( ( 𝑓𝑧 ) ∈ 𝑧 ∧ ( 𝑓𝑧 ) ∈ ran 𝑓 ) )
59 57 58 syl6ibr ( 𝑧𝑥 → ( ( ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤𝑓 Fn 𝑥 ) → ( 𝑓𝑧 ) ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
60 59 expd ( 𝑧𝑥 → ( ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 → ( 𝑓 Fn 𝑥 → ( 𝑓𝑧 ) ∈ ( 𝑧 ∩ ran 𝑓 ) ) ) )
61 60 com13 ( 𝑓 Fn 𝑥 → ( ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 → ( 𝑧𝑥 → ( 𝑓𝑧 ) ∈ ( 𝑧 ∩ ran 𝑓 ) ) ) )
62 61 imp31 ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑧𝑥 ) → ( 𝑓𝑧 ) ∈ ( 𝑧 ∩ ran 𝑓 ) )
63 eleq1 ( 𝑣 = ( 𝑓𝑧 ) → ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ ( 𝑓𝑧 ) ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
64 62 63 syl5ibrcom ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑧𝑥 ) → ( 𝑣 = ( 𝑓𝑧 ) → 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
65 64 adantr ( ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑧𝑥 ) ∧ ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ( 𝑣 = ( 𝑓𝑧 ) → 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
66 50 65 impbid ( ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑧𝑥 ) ∧ ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ( 𝑓𝑧 ) ) )
67 66 ex ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑧𝑥 ) → ( ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) → ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ( 𝑓𝑧 ) ) ) )
68 67 alrimdv ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑧𝑥 ) → ( ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) → ∀ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ( 𝑓𝑧 ) ) ) )
69 fvex ( 𝑓𝑧 ) ∈ V
70 eqeq2 ( = ( 𝑓𝑧 ) → ( 𝑣 = 𝑣 = ( 𝑓𝑧 ) ) )
71 70 bibi2d ( = ( 𝑓𝑧 ) → ( ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ) ↔ ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ( 𝑓𝑧 ) ) ) )
72 71 albidv ( = ( 𝑓𝑧 ) → ( ∀ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ) ↔ ∀ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ( 𝑓𝑧 ) ) ) )
73 69 72 spcev ( ∀ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ( 𝑓𝑧 ) ) → ∃ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ) )
74 eu6 ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ) )
75 73 74 sylibr ( ∀ 𝑣 ( 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ↔ 𝑣 = ( 𝑓𝑧 ) ) → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) )
76 68 75 syl6 ( ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ 𝑧𝑥 ) → ( ∀ 𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
77 76 ralimdva ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 ) → ( ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) → ∀ 𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
78 77 ex ( 𝑓 Fn 𝑥 → ( ∀ 𝑤𝑥 ( 𝑓𝑤 ) ∈ 𝑤 → ( ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) → ∀ 𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) ) )
79 10 78 syl5 ( 𝑓 Fn 𝑥 → ( ( ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ∧ ∀ 𝑧𝑥 𝑧 ≠ ∅ ) → ( ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) → ∀ 𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) ) )
80 79 expd ( 𝑓 Fn 𝑥 → ( ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) → ( ∀ 𝑧𝑥 𝑧 ≠ ∅ → ( ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) → ∀ 𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) ) ) )
81 80 imp4b ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ) → ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∀ 𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
82 vex 𝑓 ∈ V
83 82 rnex ran 𝑓 ∈ V
84 ineq2 ( 𝑦 = ran 𝑓 → ( 𝑧𝑦 ) = ( 𝑧 ∩ ran 𝑓 ) )
85 84 eleq2d ( 𝑦 = ran 𝑓 → ( 𝑣 ∈ ( 𝑧𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
86 85 eubidv ( 𝑦 = ran 𝑓 → ( ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
87 86 ralbidv ( 𝑦 = ran 𝑓 → ( ∀ 𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ↔ ∀ 𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) ) )
88 83 87 spcev ( ∀ 𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ran 𝑓 ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) )
89 81 88 syl6 ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ) → ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) )
90 89 exlimiv ( ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ) → ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) )
91 90 alimi ( ∀ 𝑥𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑤𝑥 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) ) → ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) )
92 1 91 sylbi ( CHOICE → ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) )
93 eqid { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 𝑢 = ( { 𝑡 } × 𝑡 ) ) } = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
94 eqid ( { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ∩ 𝑦 ) = ( { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ∩ 𝑦 )
95 biid ( ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) ↔ ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) )
96 93 94 95 dfac5lem5 ( ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) → ∃ 𝑓𝑤 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) )
97 96 alrimiv ( ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) → ∀ 𝑓𝑤 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) )
98 dfac3 ( CHOICE ↔ ∀ 𝑓𝑤 ( 𝑤 ≠ ∅ → ( 𝑓𝑤 ) ∈ 𝑤 ) )
99 97 98 sylibr ( ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) → CHOICE )
100 92 99 impbii ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧𝑥𝑤𝑥 ( 𝑧𝑤 → ( 𝑧𝑤 ) = ∅ ) ) → ∃ 𝑦𝑧𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧𝑦 ) ) )