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 CHOICExAC_x=V

Proof

Step Hyp Ref Expression
1 acacni CHOICExVAC_x=V
2 1 elvd CHOICEAC_x=V
3 2 alrimiv CHOICExAC_x=V
4 vex yV
5 4 difexi yV
6 acneq x=yAC_x=AC_y
7 6 eqeq1d x=yAC_x=VAC_y=V
8 5 7 spcv xAC_x=VAC_y=V
9 vuniex yV
10 id AC_y=VAC_y=V
11 9 10 eleqtrrid AC_y=VyAC_y
12 eldifi zyzy
13 elssuni zyzy
14 12 13 syl zyzy
15 eldifsni zyz
16 14 15 jca zyzyz
17 16 rgen zyzyz
18 acni2 yAC_yzyzyzgg:yyzygzz
19 11 17 18 sylancl AC_y=Vgg:yyzygzz
20 4 mptex xygxV
21 simpr g:yyzygzzzygzz
22 eldifsn zyzyz
23 22 imbi1i zyxygxzzzyzxygxzz
24 fveq2 x=zgx=gz
25 eqid xygx=xygx
26 fvex gzV
27 24 25 26 fvmpt zyxygxz=gz
28 12 27 syl zyxygxz=gz
29 28 eleq1d zyxygxzzgzz
30 29 pm5.74i zyxygxzzzygzz
31 impexp zyzxygxzzzyzxygxzz
32 23 30 31 3bitr3i zygzzzyzxygxzz
33 32 ralbii2 zygzzzyzxygxzz
34 21 33 sylib g:yyzygzzzyzxygxzz
35 fvrn0 gxrang
36 35 rgenw xygxrang
37 25 fmpt xygxrangxygx:yrang
38 36 37 mpbi xygx:yrang
39 ffn xygx:yrangxygxFny
40 38 39 ax-mp xygxFny
41 34 40 jctil g:yyzygzzxygxFnyzyzxygxzz
42 fneq1 f=xygxfFnyxygxFny
43 fveq1 f=xygxfz=xygxz
44 43 eleq1d f=xygxfzzxygxzz
45 44 imbi2d f=xygxzfzzzxygxzz
46 45 ralbidv f=xygxzyzfzzzyzxygxzz
47 42 46 anbi12d f=xygxfFnyzyzfzzxygxFnyzyzxygxzz
48 47 spcegv xygxVxygxFnyzyzxygxzzffFnyzyzfzz
49 20 41 48 mpsyl g:yyzygzzffFnyzyzfzz
50 49 exlimiv gg:yyzygzzffFnyzyzfzz
51 8 19 50 3syl xAC_x=VffFnyzyzfzz
52 51 alrimiv xAC_x=VyffFnyzyzfzz
53 dfac4 CHOICEyffFnyzyzfzz
54 52 53 sylibr xAC_x=VCHOICE
55 3 54 impbii CHOICExAC_x=V