Metamath Proof Explorer


Theorem dfac11

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 CHOICExfzxzfz𝒫zFin

Proof

Step Hyp Ref Expression
1 dfac3 CHOICEacdadcdd
2 raleq a=xdadcdddxdcdd
3 2 exbidv a=xcdadcddcdxdcdd
4 3 cbvalvw acdadcddxcdxdcdd
5 neeq1 d=zdz
6 fveq2 d=zcd=cz
7 id d=zd=z
8 6 7 eleq12d d=zcddczz
9 5 8 imbi12d d=zdcddzczz
10 9 cbvralvw dxdcddzxzczz
11 fveq2 b=zcb=cz
12 11 sneqd b=zcb=cz
13 eqid bxcb=bxcb
14 snex czV
15 12 13 14 fvmpt zxbxcbz=cz
16 15 3ad2ant1 zxzczzbxcbz=cz
17 simp3 zxzczzczz
18 17 snssd zxzczzczz
19 14 elpw cz𝒫zczz
20 18 19 sylibr zxzczzcz𝒫z
21 snfi czFin
22 21 a1i zxzczzczFin
23 20 22 elind zxzczzcz𝒫zFin
24 fvex czV
25 24 snnz cz
26 25 a1i zxzczzcz
27 eldifsn cz𝒫zFincz𝒫zFincz
28 23 26 27 sylanbrc zxzczzcz𝒫zFin
29 16 28 eqeltrd zxzczzbxcbz𝒫zFin
30 29 3exp zxzczzbxcbz𝒫zFin
31 30 a2d zxzczzzbxcbz𝒫zFin
32 31 ralimia zxzczzzxzbxcbz𝒫zFin
33 10 32 sylbi dxdcddzxzbxcbz𝒫zFin
34 vex xV
35 34 mptex bxcbV
36 fveq1 f=bxcbfz=bxcbz
37 36 eleq1d f=bxcbfz𝒫zFinbxcbz𝒫zFin
38 37 imbi2d f=bxcbzfz𝒫zFinzbxcbz𝒫zFin
39 38 ralbidv f=bxcbzxzfz𝒫zFinzxzbxcbz𝒫zFin
40 35 39 spcev zxzbxcbz𝒫zFinfzxzfz𝒫zFin
41 33 40 syl dxdcddfzxzfz𝒫zFin
42 41 exlimiv cdxdcddfzxzfz𝒫zFin
43 42 alimi xcdxdcddxfzxzfz𝒫zFin
44 4 43 sylbi acdadcddxfzxzfz𝒫zFin
45 1 44 sylbi CHOICExfzxzfz𝒫zFin
46 fvex R1rankaV
47 46 pwex 𝒫R1rankaV
48 raleq x=𝒫R1rankazxzfz𝒫zFinz𝒫R1rankazfz𝒫zFin
49 48 exbidv x=𝒫R1rankafzxzfz𝒫zFinfz𝒫R1rankazfz𝒫zFin
50 47 49 spcv xfzxzfz𝒫zFinfz𝒫R1rankazfz𝒫zFin
51 rankon rankaOn
52 51 a1i z𝒫R1rankazfz𝒫zFinrankaOn
53 id z𝒫R1rankazfz𝒫zFinz𝒫R1rankazfz𝒫zFin
54 52 53 aomclem8 z𝒫R1rankazfz𝒫zFinbbWeR1ranka
55 54 exlimiv fz𝒫R1rankazfz𝒫zFinbbWeR1ranka
56 vex aV
57 r1rankid aVaR1ranka
58 wess aR1rankabWeR1rankabWea
59 58 eximdv aR1rankabbWeR1rankabbWea
60 56 57 59 mp2b bbWeR1rankabbWea
61 50 55 60 3syl xfzxzfz𝒫zFinbbWea
62 61 alrimiv xfzxzfz𝒫zFinabbWea
63 dfac8 CHOICEabbWea
64 62 63 sylibr xfzxzfz𝒫zFinCHOICE
65 45 64 impbii CHOICExfzxzfz𝒫zFin