Metamath Proof Explorer


Theorem dfac13

Description: The axiom of choice holds iff every set has choice sequences as long as itself. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion dfac13 CHOICExxAC_x

Proof

Step Hyp Ref Expression
1 vex xV
2 acacni CHOICExVAC_x=V
3 2 elvd CHOICEAC_x=V
4 1 3 eleqtrrid CHOICExAC_x
5 4 alrimiv CHOICExxAC_x
6 vpwex 𝒫zV
7 id x=𝒫zx=𝒫z
8 acneq x=𝒫zAC_x=AC_𝒫z
9 7 8 eleq12d x=𝒫zxAC_x𝒫zAC_𝒫z
10 6 9 spcv xxAC_x𝒫zAC_𝒫z
11 vex yV
12 vex zV
13 12 canth2 z𝒫z
14 sdomdom z𝒫zz𝒫z
15 acndom2 z𝒫z𝒫zAC_𝒫zzAC_𝒫z
16 13 14 15 mp2b 𝒫zAC_𝒫zzAC_𝒫z
17 acnnum zAC_𝒫zzdomcard
18 16 17 sylib 𝒫zAC_𝒫zzdomcard
19 numacn yVzdomcardzAC_y
20 11 18 19 mpsyl 𝒫zAC_𝒫zzAC_y
21 10 20 syl xxAC_xzAC_y
22 12 a1i xxAC_xzV
23 21 22 2thd xxAC_xzAC_yzV
24 23 eqrdv xxAC_xAC_y=V
25 24 alrimiv xxAC_xyAC_y=V
26 dfacacn CHOICEyAC_y=V
27 25 26 sylibr xxAC_xCHOICE
28 5 27 impbii CHOICExxAC_x