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