| Step | Hyp | Ref
| Expression |
| 1 | | dfac3 10161 |
. 2
⊢
(CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 2 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑓 = 𝑦 → (𝑓‘𝑧) = (𝑦‘𝑧)) |
| 3 | 2 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑓 = 𝑦 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑦‘𝑧) ∈ 𝑧)) |
| 4 | 3 | imbi2d 340 |
. . . . . . 7
⊢ (𝑓 = 𝑦 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧))) |
| 5 | 4 | ralbidv 3178 |
. . . . . 6
⊢ (𝑓 = 𝑦 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧))) |
| 6 | 5 | cbvexvw 2036 |
. . . . 5
⊢
(∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧)) |
| 7 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑦‘𝑤) ∈ V |
| 8 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) = (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) |
| 9 | 7, 8 | fnmpti 6711 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) Fn 𝑥 |
| 10 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → (𝑦‘𝑤) = (𝑦‘𝑧)) |
| 11 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝑦‘𝑧) ∈ V |
| 12 | 10, 8, 11 | fvmpt 7016 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑥 → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) = (𝑦‘𝑧)) |
| 13 | 12 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑥 → (((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧 ↔ (𝑦‘𝑧) ∈ 𝑧)) |
| 14 | 13 | imbi2d 340 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑥 → ((𝑧 ≠ ∅ → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧))) |
| 15 | 14 | ralbiia 3091 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧)) |
| 16 | 15 | anbi2i 623 |
. . . . . . . 8
⊢ (((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧)) ↔ ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧))) |
| 17 | 9, 16 | mpbiran 709 |
. . . . . . 7
⊢ (((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧)) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧)) |
| 18 | | fvrn0 6936 |
. . . . . . . . . . 11
⊢ (𝑦‘𝑤) ∈ (ran 𝑦 ∪ {∅}) |
| 19 | 18 | rgenw 3065 |
. . . . . . . . . 10
⊢
∀𝑤 ∈
𝑥 (𝑦‘𝑤) ∈ (ran 𝑦 ∪ {∅}) |
| 20 | 8 | fmpt 7130 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
𝑥 (𝑦‘𝑤) ∈ (ran 𝑦 ∪ {∅}) ↔ (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)):𝑥⟶(ran 𝑦 ∪ {∅})) |
| 21 | 19, 20 | mpbi 230 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)):𝑥⟶(ran 𝑦 ∪ {∅}) |
| 22 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 23 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
| 24 | 23 | rnex 7932 |
. . . . . . . . . 10
⊢ ran 𝑦 ∈ V |
| 25 | | p0ex 5384 |
. . . . . . . . . 10
⊢ {∅}
∈ V |
| 26 | 24, 25 | unex 7764 |
. . . . . . . . 9
⊢ (ran
𝑦 ∪ {∅}) ∈
V |
| 27 | | fex2 7958 |
. . . . . . . . 9
⊢ (((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)):𝑥⟶(ran 𝑦 ∪ {∅}) ∧ 𝑥 ∈ V ∧ (ran 𝑦 ∪ {∅}) ∈ V) → (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) ∈ V) |
| 28 | 21, 22, 26, 27 | mp3an 1463 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) ∈ V |
| 29 | | fneq1 6659 |
. . . . . . . . 9
⊢ (𝑓 = (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) → (𝑓 Fn 𝑥 ↔ (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) Fn 𝑥)) |
| 30 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) → (𝑓‘𝑧) = ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧)) |
| 31 | 30 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) → ((𝑓‘𝑧) ∈ 𝑧 ↔ ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧)) |
| 32 | 31 | imbi2d 340 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧))) |
| 33 | 32 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑓 = (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧))) |
| 34 | 29, 33 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑓 = (𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) → ((𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧)))) |
| 35 | 28, 34 | spcev 3606 |
. . . . . . 7
⊢ (((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤)) Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ((𝑤 ∈ 𝑥 ↦ (𝑦‘𝑤))‘𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 36 | 17, 35 | sylbir 235 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 37 | 36 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑦‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 38 | 6, 37 | sylbi 217 |
. . . 4
⊢
(∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 39 | | exsimpr 1869 |
. . . 4
⊢
(∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 40 | 38, 39 | impbii 209 |
. . 3
⊢
(∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 41 | 40 | albii 1819 |
. 2
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑥∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 42 | 1, 41 | bitri 275 |
1
⊢
(CHOICE ↔ ∀𝑥∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |