This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid ⊢ ( ( 𝑓 ‘ 𝑡 ) = 𝑣 → ( 𝑧 = 𝑡 → 𝑣 = ( 𝑓 ‘ 𝑧 ) ) )
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 biimtrid ⊢ ( ( 𝑓 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 imbitrrdi ⊢ ( 𝑧 ∈ 𝑥 → ( ( ∀ 𝑤 ∈ 𝑥 ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ∧ 𝑓 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 biid ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
95 eqid ⊢ ( ∪ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ∩ 𝑦 ) = ( ∪ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ∩ 𝑦 )
96 93 94 95 dfac5lem5 ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∃ 𝑓 ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
97 96 alrimiv ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ ℎ ∃ 𝑓 ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
98 dfac3 ⊢ ( CHOICE ↔ ∀ ℎ ∃ 𝑓 ∀ 𝑤 ∈ ℎ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
99 97 98 sylibr ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → CHOICE )
100 92 99 impbii ⊢ ( CHOICE ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )