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 ↔ ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )

Proof

Step Hyp Ref Expression
1 dfac3 ( CHOICE ↔ ∀ 𝑎𝑐𝑑𝑎 ( 𝑑 ≠ ∅ → ( 𝑐𝑑 ) ∈ 𝑑 ) )
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 { ( 𝑐𝑧 ) } ∈ V
15 12 13 14 fvmpt ( 𝑧𝑥 → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) = { ( 𝑐𝑧 ) } )
16 15 3ad2ant1 ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) = { ( 𝑐𝑧 ) } )
17 simp3 ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → ( 𝑐𝑧 ) ∈ 𝑧 )
18 17 snssd ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → { ( 𝑐𝑧 ) } ⊆ 𝑧 )
19 14 elpw ( { ( 𝑐𝑧 ) } ∈ 𝒫 𝑧 ↔ { ( 𝑐𝑧 ) } ⊆ 𝑧 )
20 18 19 sylibr ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → { ( 𝑐𝑧 ) } ∈ 𝒫 𝑧 )
21 snfi { ( 𝑐𝑧 ) } ∈ Fin
22 21 a1i ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → { ( 𝑐𝑧 ) } ∈ Fin )
23 20 22 elind ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → { ( 𝑐𝑧 ) } ∈ ( 𝒫 𝑧 ∩ Fin ) )
24 fvex ( 𝑐𝑧 ) ∈ V
25 24 snnz { ( 𝑐𝑧 ) } ≠ ∅
26 25 a1i ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → { ( 𝑐𝑧 ) } ≠ ∅ )
27 eldifsn ( { ( 𝑐𝑧 ) } ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ↔ ( { ( 𝑐𝑧 ) } ∈ ( 𝒫 𝑧 ∩ Fin ) ∧ { ( 𝑐𝑧 ) } ≠ ∅ ) )
28 23 26 27 sylanbrc ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → { ( 𝑐𝑧 ) } ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) )
29 16 28 eqeltrd ( ( 𝑧𝑥𝑧 ≠ ∅ ∧ ( 𝑐𝑧 ) ∈ 𝑧 ) → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) )
30 29 3exp ( 𝑧𝑥 → ( 𝑧 ≠ ∅ → ( ( 𝑐𝑧 ) ∈ 𝑧 → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ) )
31 30 a2d ( 𝑧𝑥 → ( ( 𝑧 ≠ ∅ → ( 𝑐𝑧 ) ∈ 𝑧 ) → ( 𝑧 ≠ ∅ → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ) )
32 31 ralimia ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑐𝑧 ) ∈ 𝑧 ) → ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
33 10 32 sylbi ( ∀ 𝑑𝑥 ( 𝑑 ≠ ∅ → ( 𝑐𝑑 ) ∈ 𝑑 ) → ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
34 vex 𝑥 ∈ V
35 34 mptex ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ∈ V
36 fveq1 ( 𝑓 = ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) → ( 𝑓𝑧 ) = ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) )
37 36 eleq1d ( 𝑓 = ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) → ( ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ↔ ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
38 37 imbi2d ( 𝑓 = ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) → ( ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ↔ ( 𝑧 ≠ ∅ → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ) )
39 38 ralbidv ( 𝑓 = ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) → ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ↔ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ) )
40 35 39 spcev ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑏𝑥 ↦ { ( 𝑐𝑏 ) } ) ‘ 𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
41 33 40 syl ( ∀ 𝑑𝑥 ( 𝑑 ≠ ∅ → ( 𝑐𝑑 ) ∈ 𝑑 ) → ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
42 41 exlimiv ( ∃ 𝑐𝑑𝑥 ( 𝑑 ≠ ∅ → ( 𝑐𝑑 ) ∈ 𝑑 ) → ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
43 42 alimi ( ∀ 𝑥𝑐𝑑𝑥 ( 𝑑 ≠ ∅ → ( 𝑐𝑑 ) ∈ 𝑑 ) → ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
44 4 43 sylbi ( ∀ 𝑎𝑐𝑑𝑎 ( 𝑑 ≠ ∅ → ( 𝑐𝑑 ) ∈ 𝑑 ) → ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
45 1 44 sylbi ( CHOICE → ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
46 fvex ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ∈ V
47 46 pwex 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ∈ V
48 raleq ( 𝑥 = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) → ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ↔ ∀ 𝑧 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ) )
49 48 exbidv ( 𝑥 = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) → ( ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ↔ ∃ 𝑓𝑧 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) ) )
50 47 49 spcv ( ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → ∃ 𝑓𝑧 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
51 rankon ( rank ‘ 𝑎 ) ∈ On
52 51 a1i ( ∀ 𝑧 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → ( rank ‘ 𝑎 ) ∈ On )
53 id ( ∀ 𝑧 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → ∀ 𝑧 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )
54 52 53 aomclem8 ( ∀ 𝑧 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → ∃ 𝑏 𝑏 We ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) )
55 54 exlimiv ( ∃ 𝑓𝑧 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → ∃ 𝑏 𝑏 We ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) )
56 vex 𝑎 ∈ V
57 r1rankid ( 𝑎 ∈ V → 𝑎 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) )
58 wess ( 𝑎 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) → ( 𝑏 We ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) → 𝑏 We 𝑎 ) )
59 58 eximdv ( 𝑎 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) → ( ∃ 𝑏 𝑏 We ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) → ∃ 𝑏 𝑏 We 𝑎 ) )
60 56 57 59 mp2b ( ∃ 𝑏 𝑏 We ( 𝑅1 ‘ ( rank ‘ 𝑎 ) ) → ∃ 𝑏 𝑏 We 𝑎 )
61 50 55 60 3syl ( ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → ∃ 𝑏 𝑏 We 𝑎 )
62 61 alrimiv ( ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → ∀ 𝑎𝑏 𝑏 We 𝑎 )
63 dfac8 ( CHOICE ↔ ∀ 𝑎𝑏 𝑏 We 𝑎 )
64 62 63 sylibr ( ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) → CHOICE )
65 45 64 impbii ( CHOICE ↔ ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ ( ( 𝒫 𝑧 ∩ Fin ) ∖ { ∅ } ) ) )