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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | |
|
2 | acacni | |
|
3 | 2 | elvd | |
4 | 1 3 | eleqtrrid | |
5 | 4 | alrimiv | |
6 | vpwex | |
|
7 | id | |
|
8 | acneq | |
|
9 | 7 8 | eleq12d | |
10 | 6 9 | spcv | |
11 | vex | |
|
12 | vex | |
|
13 | 12 | canth2 | |
14 | sdomdom | |
|
15 | acndom2 | |
|
16 | 13 14 15 | mp2b | |
17 | acnnum | |
|
18 | 16 17 | sylib | |
19 | numacn | |
|
20 | 11 18 19 | mpsyl | |
21 | 10 20 | syl | |
22 | 12 | a1i | |
23 | 21 22 | 2thd | |
24 | 23 | eqrdv | |
25 | 24 | alrimiv | |
26 | dfacacn | |
|
27 | 25 26 | sylibr | |
28 | 5 27 | impbii | |