Description: The right-hand side of this theorem (compare with ac4 ), sometimes known as the "axiom of multiple choice", is a choice equivalent. Curiously, this statement cannot be proved without ax-reg , despite not mentioning the cumulative hierarchy in any way as most consequences of regularity do.
This is definition (MC) of Schechter p. 141.EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it.
A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well-ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015) (Revised by Stefan O'Rear, 1-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | dfac11 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfac3 | |
|
2 | raleq | |
|
3 | 2 | exbidv | |
4 | 3 | cbvalvw | |
5 | neeq1 | |
|
6 | fveq2 | |
|
7 | id | |
|
8 | 6 7 | eleq12d | |
9 | 5 8 | imbi12d | |
10 | 9 | cbvralvw | |
11 | fveq2 | |
|
12 | 11 | sneqd | |
13 | eqid | |
|
14 | snex | |
|
15 | 12 13 14 | fvmpt | |
16 | 15 | 3ad2ant1 | |
17 | simp3 | |
|
18 | 17 | snssd | |
19 | 14 | elpw | |
20 | 18 19 | sylibr | |
21 | snfi | |
|
22 | 21 | a1i | |
23 | 20 22 | elind | |
24 | fvex | |
|
25 | 24 | snnz | |
26 | 25 | a1i | |
27 | eldifsn | |
|
28 | 23 26 27 | sylanbrc | |
29 | 16 28 | eqeltrd | |
30 | 29 | 3exp | |
31 | 30 | a2d | |
32 | 31 | ralimia | |
33 | 10 32 | sylbi | |
34 | vex | |
|
35 | 34 | mptex | |
36 | fveq1 | |
|
37 | 36 | eleq1d | |
38 | 37 | imbi2d | |
39 | 38 | ralbidv | |
40 | 35 39 | spcev | |
41 | 33 40 | syl | |
42 | 41 | exlimiv | |
43 | 42 | alimi | |
44 | 4 43 | sylbi | |
45 | 1 44 | sylbi | |
46 | fvex | |
|
47 | 46 | pwex | |
48 | raleq | |
|
49 | 48 | exbidv | |
50 | 47 49 | spcv | |
51 | rankon | |
|
52 | 51 | a1i | |
53 | id | |
|
54 | 52 53 | aomclem8 | |
55 | 54 | exlimiv | |
56 | vex | |
|
57 | r1rankid | |
|
58 | wess | |
|
59 | 58 | eximdv | |
60 | 56 57 59 | mp2b | |
61 | 50 55 60 | 3syl | |
62 | 61 | alrimiv | |
63 | dfac8 | |
|
64 | 62 63 | sylibr | |
65 | 45 64 | impbii | |