Metamath Proof Explorer

Theorem dfac4

Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Axiom AC of BellMachover p. 488. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004) (Revised by Mario Carneiro, 26-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 dfac3 ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
2 fveq1 ⊢ ( 𝑓 = 𝑦 → ( 𝑓 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) )
3 2 eleq1d ⊢ ( 𝑓 = 𝑦 → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) )
4 3 imbi2d ⊢ ( 𝑓 = 𝑦 → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) ) )
5 4 ralbidv ⊢ ( 𝑓 = 𝑦 → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) ) )
6 5 cbvexvw ⊢ ( ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) )
7 fvex ⊢ ( 𝑦 ‘ 𝑤 ) ∈ V
8 eqid ⊢ ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) = ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) )
9 7 8 fnmpti ⊢ ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) Fn 𝑥
10 fveq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑦 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑧 ) )
11 fvex ⊢ ( 𝑦 ‘ 𝑧 ) ∈ V
12 10 8 11 fvmpt ⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) )
13 12 eleq1d ⊢ ( 𝑧 ∈ 𝑥 → ( ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) )
14 13 imbi2d ⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ≠ ∅ → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) ) )
15 14 ralbiia ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) )
16 15 anbi2i ⊢ ( ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) ↔ ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) ) )
17 9 16 mpbiran ⊢ ( ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) )
18 fvrn0 ⊢ ( 𝑦 ‘ 𝑤 ) ∈ ( ran 𝑦 ∪ { ∅ } )
19 18 rgenw ⊢ ∀ 𝑤 ∈ 𝑥 ( 𝑦 ‘ 𝑤 ) ∈ ( ran 𝑦 ∪ { ∅ } )
20 8 fmpt ⊢ ( ∀ 𝑤 ∈ 𝑥 ( 𝑦 ‘ 𝑤 ) ∈ ( ran 𝑦 ∪ { ∅ } ) ↔ ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) : 𝑥 ⟶ ( ran 𝑦 ∪ { ∅ } ) )
21 19 20 mpbi ⊢ ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) : 𝑥 ⟶ ( ran 𝑦 ∪ { ∅ } )
22 vex ⊢ 𝑥 ∈ V
23 vex ⊢ 𝑦 ∈ V
24 23 rnex ⊢ ran 𝑦 ∈ V
25 p0ex ⊢ { ∅ } ∈ V
26 24 25 unex ⊢ ( ran 𝑦 ∪ { ∅ } ) ∈ V
27 fex2 ⊢ ( ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) : 𝑥 ⟶ ( ran 𝑦 ∪ { ∅ } ) ∧ 𝑥 ∈ V ∧ ( ran 𝑦 ∪ { ∅ } ) ∈ V ) → ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ∈ V )
28 21 22 26 27 mp3an ⊢ ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ∈ V
29 fneq1 ⊢ ( 𝑓 = ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) → ( 𝑓 Fn 𝑥 ↔ ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) Fn 𝑥 ) )
30 fveq1 ⊢ ( 𝑓 = ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) → ( 𝑓 ‘ 𝑧 ) = ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) )
31 30 eleq1d ⊢ ( 𝑓 = ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
32 31 imbi2d ⊢ ( 𝑓 = ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
33 32 ralbidv ⊢ ( 𝑓 = ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
34 29 33 anbi12d ⊢ ( 𝑓 = ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ↔ ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) ) )
35 28 34 spcev ⊢ ( ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑤 ∈ 𝑥 ↦ ( 𝑦 ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
36 17 35 sylbir ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
37 36 exlimiv ⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑦 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
38 6 37 sylbi ⊢ ( ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
39 exsimpr ⊢ ( ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
40 38 39 impbii ⊢ ( ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
41 40 albii ⊢ ( ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑥 ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
42 1 41 bitri ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )