Metamath Proof Explorer

Theorem dfacacn

Description: A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dfacacn ( CHOICE ↔ ∀ 𝑥 AC 𝑥 = V )

Proof

Step Hyp Ref Expression
1 acacni ⊢ ( ( CHOICE ∧ 𝑥 ∈ V ) → AC 𝑥 = V )
2 1 elvd ⊢ ( CHOICE → AC 𝑥 = V )
3 2 alrimiv ⊢ ( CHOICE → ∀ 𝑥 AC 𝑥 = V )
4 vex ⊢ 𝑦 ∈ V
5 4 difexi ⊢ ( 𝑦 ∖ { ∅ } ) ∈ V
6 acneq ⊢ ( 𝑥 = ( 𝑦 ∖ { ∅ } ) → AC 𝑥 = AC ( 𝑦 ∖ { ∅ } ) )
7 6 eqeq1d ⊢ ( 𝑥 = ( 𝑦 ∖ { ∅ } ) → ( AC 𝑥 = V ↔ AC ( 𝑦 ∖ { ∅ } ) = V ) )
8 5 7 spcv ⊢ ( ∀ 𝑥 AC 𝑥 = V → AC ( 𝑦 ∖ { ∅ } ) = V )
9 vuniex ⊢ ∪ 𝑦 ∈ V
10 id ⊢ ( AC ( 𝑦 ∖ { ∅ } ) = V → AC ( 𝑦 ∖ { ∅ } ) = V )
11 9 10 eleqtrrid ⊢ ( AC ( 𝑦 ∖ { ∅ } ) = V → ∪ 𝑦 ∈ AC ( 𝑦 ∖ { ∅ } ) )
12 eldifi ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → 𝑧 ∈ 𝑦 )
13 elssuni ⊢ ( 𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦 )
14 12 13 syl ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → 𝑧 ⊆ ∪ 𝑦 )
15 eldifsni ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → 𝑧 ≠ ∅ )
16 14 15 jca ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( 𝑧 ⊆ ∪ 𝑦 ∧ 𝑧 ≠ ∅ ) )
17 16 rgen ⊢ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑧 ⊆ ∪ 𝑦 ∧ 𝑧 ≠ ∅ )
18 acni2 ⊢ ( ( ∪ 𝑦 ∈ AC ( 𝑦 ∖ { ∅ } ) ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑧 ⊆ ∪ 𝑦 ∧ 𝑧 ≠ ∅ ) ) → ∃ 𝑔 ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
19 11 17 18 sylancl ⊢ ( AC ( 𝑦 ∖ { ∅ } ) = V → ∃ 𝑔 ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
20 4 mptex ⊢ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ∈ V
21 eldifsn ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅ ) )
22 21 imbi1i ⊢ ( ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
23 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑧 ) )
24 eqid ⊢ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) )
25 fvex ⊢ ( 𝑔 ‘ 𝑧 ) ∈ V
26 23 24 25 fvmpt ⊢ ( 𝑧 ∈ 𝑦 → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
27 12 26 syl ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
28 27 eleq1d ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
29 28 pm5.74i ⊢ ( ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
30 impexp ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
31 22 29 30 3bitr3i ⊢ ( ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
32 31 ralbii2 ⊢ ( ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ↔ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
33 32 bilani ⊢ ( ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
34 fvrn0 ⊢ ( 𝑔 ‘ 𝑥 ) ∈ ( ran 𝑔 ∪ { ∅ } )
35 34 rgenw ⊢ ∀ 𝑥 ∈ 𝑦 ( 𝑔 ‘ 𝑥 ) ∈ ( ran 𝑔 ∪ { ∅ } )
36 24 fmpt ⊢ ( ∀ 𝑥 ∈ 𝑦 ( 𝑔 ‘ 𝑥 ) ∈ ( ran 𝑔 ∪ { ∅ } ) ↔ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) : 𝑦 ⟶ ( ran 𝑔 ∪ { ∅ } ) )
37 35 36 mpbi ⊢ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) : 𝑦 ⟶ ( ran 𝑔 ∪ { ∅ } )
38 ffn ⊢ ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) : 𝑦 ⟶ ( ran 𝑔 ∪ { ∅ } ) → ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 )
39 37 38 ax-mp ⊢ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦
40 33 39 jctil ⊢ ( ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
41 fneq1 ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( 𝑓 Fn 𝑦 ↔ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 ) )
42 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( 𝑓 ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) )
43 42 eleq1d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
44 43 imbi2d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
45 44 ralbidv ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
46 41 45 anbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) ) )
47 46 spcegv ⊢ ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ∈ V → ( ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ) )
48 20 40 47 mpsyl ⊢ ( ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
49 48 exlimiv ⊢ ( ∃ 𝑔 ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
50 8 19 49 3syl ⊢ ( ∀ 𝑥 AC 𝑥 = V → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
51 50 alrimiv ⊢ ( ∀ 𝑥 AC 𝑥 = V → ∀ 𝑦 ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
52 dfac4 ⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
53 51 52 sylibr ⊢ ( ∀ 𝑥 AC 𝑥 = V → CHOICE )
54 3 53 impbii ⊢ ( CHOICE ↔ ∀ 𝑥 AC 𝑥 = V )