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 ) ∖ { ∅ } ) ) ) |
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 ) ∖ { ∅ } ) ) ) |