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 ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅

Proof

Step Hyp Ref Expression
1 dfac3 ⊢ CHOICE ↔ ∀ a ∃ c ∀ d ∈ a d ≠ ∅ → c ⁡ d ∈ d
2 raleq ⊢ a = x → ∀ d ∈ a d ≠ ∅ → c ⁡ d ∈ d ↔ ∀ d ∈ x d ≠ ∅ → c ⁡ d ∈ d
3 2 exbidv ⊢ a = x → ∃ c ∀ d ∈ a d ≠ ∅ → c ⁡ d ∈ d ↔ ∃ c ∀ d ∈ x d ≠ ∅ → c ⁡ d ∈ d
4 3 cbvalvw ⊢ ∀ a ∃ c ∀ d ∈ a d ≠ ∅ → c ⁡ d ∈ d ↔ ∀ x ∃ c ∀ d ∈ x d ≠ ∅ → 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 ∈ x d ≠ ∅ → c ⁡ d ∈ d ↔ ∀ z ∈ x z ≠ ∅ → 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 ∈ x z ≠ ∅ → c ⁡ z ∈ z → ∀ z ∈ x z ≠ ∅ → b ∈ x ⟼ c ⁡ b ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
33 10 32 sylbi ⊢ ∀ d ∈ x d ≠ ∅ → c ⁡ d ∈ d → ∀ z ∈ x z ≠ ∅ → 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 ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ ↔ ∀ z ∈ x z ≠ ∅ → b ∈ x ⟼ c ⁡ b ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
40 35 39 spcev ⊢ ∀ z ∈ x z ≠ ∅ → b ∈ x ⟼ c ⁡ b ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
41 33 40 syl ⊢ ∀ d ∈ x d ≠ ∅ → c ⁡ d ∈ d → ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
42 41 exlimiv ⊢ ∃ c ∀ d ∈ x d ≠ ∅ → c ⁡ d ∈ d → ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
43 42 alimi ⊢ ∀ x ∃ c ∀ d ∈ x d ≠ ∅ → c ⁡ d ∈ d → ∀ x ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
44 4 43 sylbi ⊢ ∀ a ∃ c ∀ d ∈ a d ≠ ∅ → c ⁡ d ∈ d → ∀ x ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
45 1 44 sylbi ⊢ CHOICE → ∀ x ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
46 fvex ⊢ R1 ⁡ rank ⁡ a ∈ V
47 46 pwex ⊢ 𝒫 R1 ⁡ rank ⁡ a ∈ V
48 raleq ⊢ x = 𝒫 R1 ⁡ rank ⁡ a → ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ ↔ ∀ z ∈ 𝒫 R1 ⁡ rank ⁡ a z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
49 48 exbidv ⊢ x = 𝒫 R1 ⁡ rank ⁡ a → ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ ↔ ∃ f ∀ z ∈ 𝒫 R1 ⁡ rank ⁡ a z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
50 47 49 spcv ⊢ ∀ x ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → ∃ f ∀ z ∈ 𝒫 R1 ⁡ rank ⁡ a z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
51 rankon ⊢ rank ⁡ a ∈ On
52 51 a1i ⊢ ∀ z ∈ 𝒫 R1 ⁡ rank ⁡ a z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → rank ⁡ a ∈ On
53 id ⊢ ∀ z ∈ 𝒫 R1 ⁡ rank ⁡ a z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → ∀ z ∈ 𝒫 R1 ⁡ rank ⁡ a z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅
54 52 53 aomclem8 ⊢ ∀ z ∈ 𝒫 R1 ⁡ rank ⁡ a z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → ∃ b b We R1 ⁡ rank ⁡ a
55 54 exlimiv ⊢ ∃ f ∀ z ∈ 𝒫 R1 ⁡ rank ⁡ a z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → ∃ b b We R1 ⁡ rank ⁡ a
56 vex ⊢ a ∈ V
57 r1rankid ⊢ a ∈ V → a ⊆ R1 ⁡ rank ⁡ a
58 wess ⊢ a ⊆ R1 ⁡ rank ⁡ a → b We R1 ⁡ rank ⁡ a → b We a
59 58 eximdv ⊢ a ⊆ R1 ⁡ rank ⁡ a → ∃ b b We R1 ⁡ rank ⁡ a → ∃ b b We a
60 56 57 59 mp2b ⊢ ∃ b b We R1 ⁡ rank ⁡ a → ∃ b b We a
61 50 55 60 3syl ⊢ ∀ x ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → ∃ b b We a
62 61 alrimiv ⊢ ∀ x ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → ∀ a ∃ b b We a
63 dfac8 ⊢ CHOICE ↔ ∀ a ∃ b b We a
64 62 63 sylibr ⊢ ∀ x ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅ → CHOICE
65 45 64 impbii ⊢ CHOICE ↔ ∀ x ∃ f ∀ z ∈ x z ≠ ∅ → f ⁡ z ∈ 𝒫 z ∩ Fin ∖ ∅