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 simpr ⊢ ( ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 )
22 eldifsn ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅ ) )
23 22 imbi1i ⊢ ( ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( ( 𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
24 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑧 ) )
25 eqid ⊢ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) )
26 fvex ⊢ ( 𝑔 ‘ 𝑧 ) ∈ V
27 24 25 26 fvmpt ⊢ ( 𝑧 ∈ 𝑦 → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
28 12 27 syl ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
29 28 eleq1d ⊢ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
30 29 pm5.74i ⊢ ( ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
31 impexp ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑧 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
32 23 30 31 3bitr3i ⊢ ( ( 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ∈ 𝑦 → ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
33 32 ralbii2 ⊢ ( ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ↔ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
34 21 33 sylib ⊢ ( ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
35 fvrn0 ⊢ ( 𝑔 ‘ 𝑥 ) ∈ ( ran 𝑔 ∪ { ∅ } )
36 35 rgenw ⊢ ∀ 𝑥 ∈ 𝑦 ( 𝑔 ‘ 𝑥 ) ∈ ( ran 𝑔 ∪ { ∅ } )
37 25 fmpt ⊢ ( ∀ 𝑥 ∈ 𝑦 ( 𝑔 ‘ 𝑥 ) ∈ ( ran 𝑔 ∪ { ∅ } ) ↔ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) : 𝑦 ⟶ ( ran 𝑔 ∪ { ∅ } ) )
38 36 37 mpbi ⊢ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) : 𝑦 ⟶ ( ran 𝑔 ∪ { ∅ } )
39 ffn ⊢ ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) : 𝑦 ⟶ ( ran 𝑔 ∪ { ∅ } ) → ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 )
40 38 39 ax-mp ⊢ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦
41 34 40 jctil ⊢ ( ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
42 fneq1 ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( 𝑓 Fn 𝑦 ↔ ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 ) )
43 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( 𝑓 ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) )
44 43 eleq1d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
45 44 imbi2d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
46 45 ralbidv ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
47 42 46 anbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) → ( ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) ) )
48 47 spcegv ⊢ ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ∈ V → ( ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( ( 𝑥 ∈ 𝑦 ↦ ( 𝑔 ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ) )
49 20 41 48 mpsyl ⊢ ( ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
50 49 exlimiv ⊢ ( ∃ 𝑔 ( 𝑔 : ( 𝑦 ∖ { ∅ } ) ⟶ ∪ 𝑦 ∧ ∀ 𝑧 ∈ ( 𝑦 ∖ { ∅ } ) ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
51 8 19 50 3syl ⊢ ( ∀ 𝑥 AC 𝑥 = V → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
52 51 alrimiv ⊢ ( ∀ 𝑥 AC 𝑥 = V → ∀ 𝑦 ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
53 dfac4 ⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
54 52 53 sylibr ⊢ ( ∀ 𝑥 AC 𝑥 = V → CHOICE )
55 3 54 impbii ⊢ ( CHOICE ↔ ∀ 𝑥 AC 𝑥 = V )