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 ⊢CHOICE↔∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅

Proof

Step Hyp Ref Expression
1 dfac3 ⊢CHOICE↔∀a∃c∀d∈ad≠∅→c⁡d∈d
2 raleq ⊢a=x→∀d∈ad≠∅→c⁡d∈d↔∀d∈xd≠∅→c⁡d∈d
3 2 exbidv ⊢a=x→∃c∀d∈ad≠∅→c⁡d∈d↔∃c∀d∈xd≠∅→c⁡d∈d
4 3 cbvalvw ⊢∀a∃c∀d∈ad≠∅→c⁡d∈d↔∀x∃c∀d∈xd≠∅→c⁡d∈d
5 neeq1 ⊢d=z→d≠∅↔z≠∅
6 fveq2 ⊢d=z→c⁡d=c⁡z
7 id ⊢d=z→d=z
8 6 7 eleq12d ⊢d=z→c⁡d∈d↔c⁡z∈z
9 5 8 imbi12d ⊢d=z→d≠∅→c⁡d∈d↔z≠∅→c⁡z∈z
10 9 cbvralvw ⊢∀d∈xd≠∅→c⁡d∈d↔∀z∈xz≠∅→c⁡z∈z
11 fveq2 ⊢b=z→c⁡b=c⁡z
12 11 sneqd ⊢b=z→c⁡b=c⁡z
13 eqid ⊢b∈x⟼c⁡b=b∈x⟼c⁡b
14 snex ⊢c⁡z∈V
15 12 13 14 fvmpt ⊢z∈x→b∈x⟼c⁡b⁡z=c⁡z
16 15 3ad2ant1 ⊢z∈x∧z≠∅∧c⁡z∈z→b∈x⟼c⁡b⁡z=c⁡z
17 simp3 ⊢z∈x∧z≠∅∧c⁡z∈z→c⁡z∈z
18 17 snssd ⊢z∈x∧z≠∅∧c⁡z∈z→c⁡z⊆z
19 14 elpw ⊢c⁡z∈𝒫z↔c⁡z⊆z
20 18 19 sylibr ⊢z∈x∧z≠∅∧c⁡z∈z→c⁡z∈𝒫z
21 snfi ⊢c⁡z∈Fin
22 21 a1i ⊢z∈x∧z≠∅∧c⁡z∈z→c⁡z∈Fin
23 20 22 elind ⊢z∈x∧z≠∅∧c⁡z∈z→c⁡z∈𝒫z∩Fin
24 fvex ⊢c⁡z∈V
25 24 snnz ⊢c⁡z≠∅
26 25 a1i ⊢z∈x∧z≠∅∧c⁡z∈z→c⁡z≠∅
27 eldifsn ⊢c⁡z∈𝒫z∩Fin∖∅↔c⁡z∈𝒫z∩Fin∧c⁡z≠∅
28 23 26 27 sylanbrc ⊢z∈x∧z≠∅∧c⁡z∈z→c⁡z∈𝒫z∩Fin∖∅
29 16 28 eqeltrd ⊢z∈x∧z≠∅∧c⁡z∈z→b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅
30 29 3exp ⊢z∈x→z≠∅→c⁡z∈z→b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅
31 30 a2d ⊢z∈x→z≠∅→c⁡z∈z→z≠∅→b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅
32 31 ralimia ⊢∀z∈xz≠∅→c⁡z∈z→∀z∈xz≠∅→b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅
33 10 32 sylbi ⊢∀d∈xd≠∅→c⁡d∈d→∀z∈xz≠∅→b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅
34 vex ⊢x∈V
35 34 mptex ⊢b∈x⟼c⁡b∈V
36 fveq1 ⊢f=b∈x⟼c⁡b→f⁡z=b∈x⟼c⁡b⁡z
37 36 eleq1d ⊢f=b∈x⟼c⁡b→f⁡z∈𝒫z∩Fin∖∅↔b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅
38 37 imbi2d ⊢f=b∈x⟼c⁡b→z≠∅→f⁡z∈𝒫z∩Fin∖∅↔z≠∅→b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅
39 38 ralbidv ⊢f=b∈x⟼c⁡b→∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅↔∀z∈xz≠∅→b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅
40 35 39 spcev ⊢∀z∈xz≠∅→b∈x⟼c⁡b⁡z∈𝒫z∩Fin∖∅→∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅
41 33 40 syl ⊢∀d∈xd≠∅→c⁡d∈d→∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅
42 41 exlimiv ⊢∃c∀d∈xd≠∅→c⁡d∈d→∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅
43 42 alimi ⊢∀x∃c∀d∈xd≠∅→c⁡d∈d→∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅
44 4 43 sylbi ⊢∀a∃c∀d∈ad≠∅→c⁡d∈d→∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅
45 1 44 sylbi ⊢CHOICE→∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅
46 fvex ⊢R1⁡rank⁡a∈V
47 46 pwex ⊢𝒫R1⁡rank⁡a∈V
48 raleq ⊢x=𝒫R1⁡rank⁡a→∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅↔∀z∈𝒫R1⁡rank⁡az≠∅→f⁡z∈𝒫z∩Fin∖∅
49 48 exbidv ⊢x=𝒫R1⁡rank⁡a→∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅↔∃f∀z∈𝒫R1⁡rank⁡az≠∅→f⁡z∈𝒫z∩Fin∖∅
50 47 49 spcv ⊢∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅→∃f∀z∈𝒫R1⁡rank⁡az≠∅→f⁡z∈𝒫z∩Fin∖∅
51 rankon ⊢rank⁡a∈On
52 51 a1i ⊢∀z∈𝒫R1⁡rank⁡az≠∅→f⁡z∈𝒫z∩Fin∖∅→rank⁡a∈On
53 id ⊢∀z∈𝒫R1⁡rank⁡az≠∅→f⁡z∈𝒫z∩Fin∖∅→∀z∈𝒫R1⁡rank⁡az≠∅→f⁡z∈𝒫z∩Fin∖∅
54 52 53 aomclem8 ⊢∀z∈𝒫R1⁡rank⁡az≠∅→f⁡z∈𝒫z∩Fin∖∅→∃bbWeR1⁡rank⁡a
55 54 exlimiv ⊢∃f∀z∈𝒫R1⁡rank⁡az≠∅→f⁡z∈𝒫z∩Fin∖∅→∃bbWeR1⁡rank⁡a
56 vex ⊢a∈V
57 r1rankid ⊢a∈V→a⊆R1⁡rank⁡a
58 wess ⊢a⊆R1⁡rank⁡a→bWeR1⁡rank⁡a→bWea
59 58 eximdv ⊢a⊆R1⁡rank⁡a→∃bbWeR1⁡rank⁡a→∃bbWea
60 56 57 59 mp2b ⊢∃bbWeR1⁡rank⁡a→∃bbWea
61 50 55 60 3syl ⊢∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅→∃bbWea
62 61 alrimiv ⊢∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅→∀a∃bbWea
63 dfac8 ⊢CHOICE↔∀a∃bbWea
64 62 63 sylibr ⊢∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅→CHOICE
65 45 64 impbii ⊢CHOICE↔∀x∃f∀z∈xz≠∅→f⁡z∈𝒫z∩Fin∖∅