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

Metamath Proof Explorer

Theorem dfac3

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as the Axiom of Choice (first form) of Enderton p. 49. The right-hand side is the Axiom of Choice of TakeutiZaring p. 83. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004) (Revised by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion dfac3 ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 df-ac ⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) )
2 vex ⊢ 𝑥 ∈ V
3 vuniex ⊢ ∪ 𝑥 ∈ V
4 2 3 xpex ⊢ ( 𝑥 × ∪ 𝑥 ) ∈ V
5 simpl ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) → 𝑤 ∈ 𝑥 )
6 elunii ⊢ ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑣 ∈ ∪ 𝑥 )
7 6 ancoms ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ∈ ∪ 𝑥 )
8 5 7 jca ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) → ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥 ) )
9 8 ssopab2i ⊢ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥 ) }
10 df-xp ⊢ ( 𝑥 × ∪ 𝑥 ) = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥 ) }
11 9 10 sseqtrri ⊢ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ⊆ ( 𝑥 × ∪ 𝑥 )
12 4 11 ssexi ⊢ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∈ V
13 sseq2 ⊢ ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → ( 𝑓 ⊆ 𝑦 ↔ 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) )
14 dmeq ⊢ ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → dom 𝑦 = dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } )
15 14 fneq2d ⊢ ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → ( 𝑓 Fn dom 𝑦 ↔ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) )
16 13 15 anbi12d ⊢ ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → ( ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) ↔ ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) ) )
17 16 exbidv ⊢ ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → ( ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) ↔ ∃ 𝑓 ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) ) )
18 12 17 spcv ⊢ ( ∀ 𝑦 ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) → ∃ 𝑓 ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) )
19 fndm ⊢ ( 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → dom 𝑓 = dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } )
20 dmopab ⊢ dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } = { 𝑤 ∣ ∃ 𝑣 ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) }
21 20 eleq2i ⊢ ( 𝑧 ∈ dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ↔ 𝑧 ∈ { 𝑤 ∣ ∃ 𝑣 ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } )
22 vex ⊢ 𝑧 ∈ V
23 elequ1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
24 eleq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑣 ∈ 𝑤 ↔ 𝑣 ∈ 𝑧 ) )
25 23 24 anbi12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧 ) ) )
26 25 exbidv ⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑣 ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧 ) ) )
27 22 26 elab ⊢ ( 𝑧 ∈ { 𝑤 ∣ ∃ 𝑣 ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧 ) )
28 19.42v ⊢ ( ∃ 𝑣 ( 𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧 ) ↔ ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑣 𝑣 ∈ 𝑧 ) )
29 n0 ⊢ ( 𝑧 ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ 𝑧 )
30 29 anbi2i ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ↔ ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑣 𝑣 ∈ 𝑧 ) )
31 28 30 bitr4i ⊢ ( ∃ 𝑣 ( 𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧 ) ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) )
32 21 27 31 3bitrri ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ↔ 𝑧 ∈ dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } )
33 eleq2 ⊢ ( dom 𝑓 = dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → ( 𝑧 ∈ dom 𝑓 ↔ 𝑧 ∈ dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) )
34 32 33 bitr4id ⊢ ( dom 𝑓 = dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ↔ 𝑧 ∈ dom 𝑓 ) )
35 19 34 syl ⊢ ( 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ↔ 𝑧 ∈ dom 𝑓 ) )
36 35 adantl ⊢ ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ↔ 𝑧 ∈ dom 𝑓 ) )
37 fnfun ⊢ ( 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } → Fun 𝑓 )
38 funfvima3 ⊢ ( ( Fun 𝑓 ∧ 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) → ( 𝑧 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) ) )
39 38 ancoms ⊢ ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ Fun 𝑓 ) → ( 𝑧 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) ) )
40 37 39 sylan2 ⊢ ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) → ( 𝑧 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) ) )
41 36 40 sylbid ⊢ ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ( 𝑓 ‘ 𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) ) )
42 41 imp ⊢ ( ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ) → ( 𝑓 ‘ 𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) )
43 imasng ⊢ ( 𝑧 ∈ V → ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) = { 𝑢 ∣ 𝑧 { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } 𝑢 } )
44 43 elv ⊢ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) = { 𝑢 ∣ 𝑧 { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } 𝑢 }
45 vex ⊢ 𝑢 ∈ V
46 elequ1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 ∈ 𝑧 ↔ 𝑢 ∈ 𝑧 ) )
47 46 anbi2d ⊢ ( 𝑣 = 𝑢 → ( ( 𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧 ) ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧 ) ) )
48 eqid ⊢ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) }
49 22 45 25 47 48 brab ⊢ ( 𝑧 { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } 𝑢 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧 ) )
50 49 abbii ⊢ { 𝑢 ∣ 𝑧 { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } 𝑢 } = { 𝑢 ∣ ( 𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧 ) }
51 44 50 eqtri ⊢ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) = { 𝑢 ∣ ( 𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧 ) }
52 ibar ⊢ ( 𝑧 ∈ 𝑥 → ( 𝑢 ∈ 𝑧 ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧 ) ) )
53 52 eqabdv ⊢ ( 𝑧 ∈ 𝑥 → 𝑧 = { 𝑢 ∣ ( 𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧 ) } )
54 51 53 eqtr4id ⊢ ( 𝑧 ∈ 𝑥 → ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) = 𝑧 )
55 54 eleq2d ⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑓 ‘ 𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) ↔ ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
56 55 ad2antrl ⊢ ( ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ) → ( ( 𝑓 ‘ 𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } “ { 𝑧 } ) ↔ ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
57 42 56 mpbid ⊢ ( ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ) → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 )
58 57 exp32 ⊢ ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) → ( 𝑧 ∈ 𝑥 → ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
59 58 ralrimiv ⊢ ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
60 59 eximi ⊢ ( ∃ 𝑓 ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤 ) } ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
61 18 60 syl ⊢ ( ∀ 𝑦 ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
62 61 alrimiv ⊢ ( ∀ 𝑦 ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) → ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
63 eqid ⊢ ( 𝑤 ∈ dom 𝑦 ↦ ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) ) = ( 𝑤 ∈ dom 𝑦 ↦ ( 𝑓 ‘ { 𝑢 ∣ 𝑤 𝑦 𝑢 } ) )
64 63 aceq3lem ⊢ ( ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) )
65 64 alrimiv ⊢ ( ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑦 ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) )
66 62 65 impbii ⊢ ( ∀ 𝑦 ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) ↔ ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
67 1 66 bitri ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )