Description: A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | dfacacn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | acacni | |
|
2 | 1 | elvd | |
3 | 2 | alrimiv | |
4 | vex | |
|
5 | 4 | difexi | |
6 | acneq | |
|
7 | 6 | eqeq1d | |
8 | 5 7 | spcv | |
9 | vuniex | |
|
10 | id | |
|
11 | 9 10 | eleqtrrid | |
12 | eldifi | |
|
13 | elssuni | |
|
14 | 12 13 | syl | |
15 | eldifsni | |
|
16 | 14 15 | jca | |
17 | 16 | rgen | |
18 | acni2 | |
|
19 | 11 17 18 | sylancl | |
20 | 4 | mptex | |
21 | simpr | |
|
22 | eldifsn | |
|
23 | 22 | imbi1i | |
24 | fveq2 | |
|
25 | eqid | |
|
26 | fvex | |
|
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 | |
|
36 | 35 | rgenw | |
37 | 25 | fmpt | |
38 | 36 37 | mpbi | |
39 | ffn | |
|
40 | 38 39 | ax-mp | |
41 | 34 40 | jctil | |
42 | fneq1 | |
|
43 | fveq1 | |
|
44 | 43 | eleq1d | |
45 | 44 | imbi2d | |
46 | 45 | ralbidv | |
47 | 42 46 | anbi12d | |
48 | 47 | spcegv | |
49 | 20 41 48 | mpsyl | |
50 | 49 | exlimiv | |
51 | 8 19 50 | 3syl | |
52 | 51 | alrimiv | |
53 | dfac4 | |
|
54 | 52 53 | sylibr | |
55 | 3 54 | impbii | |