| Step | Hyp | Ref
| Expression |
| 1 | | dfac3 10161 |
. 2
⊢
(CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 2 | | nfra1 3284 |
. . . . . 6
⊢
Ⅎ𝑧∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) |
| 3 | | rsp 3247 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 4 | | equid 2011 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 = 𝑧 |
| 5 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅)) |
| 6 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑧 → (𝑢 = 𝑧 ↔ 𝑧 = 𝑧)) |
| 7 | 5, 6 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) ↔ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧))) |
| 8 | 7 | rspcev 3622 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ 𝑥 ∧ (𝑧 ≠ ∅ ∧ 𝑧 = 𝑧)) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧)) |
| 9 | 4, 8 | mpanr2 704 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧)) |
| 10 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧)) |
| 11 | 10 | preq1d 4739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑧 → {(𝑓‘𝑢), 𝑢} = {(𝑓‘𝑧), 𝑢}) |
| 12 | | preq2 4734 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑢} = {(𝑓‘𝑧), 𝑧}) |
| 13 | 11, 12 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑧 → {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}) |
| 14 | 13 | anim2i 617 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})) |
| 15 | 14 | reximi 3084 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢 ∈
𝑥 (𝑢 ≠ ∅ ∧ 𝑢 = 𝑧) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})) |
| 16 | 9, 15 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})) |
| 17 | | prex 5437 |
. . . . . . . . . . . . . . . . 17
⊢ {(𝑓‘𝑧), 𝑧} ∈ V |
| 18 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})) |
| 19 | 18 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))) |
| 20 | 19 | rexbidv 3179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = {(𝑓‘𝑧), 𝑧} → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢}))) |
| 21 | 17, 20 | elab 3679 |
. . . . . . . . . . . . . . . 16
⊢ ({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ {(𝑓‘𝑧), 𝑧} = {(𝑓‘𝑢), 𝑢})) |
| 22 | 16, 21 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → {(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})}) |
| 23 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
| 24 | 23 | prid2 4763 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ {(𝑓‘𝑧), 𝑧} |
| 25 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓‘𝑧) ∈ V |
| 26 | 25 | prid1 4762 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧} |
| 27 | 24, 26 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}) |
| 28 | | eleq2 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑧), 𝑧})) |
| 29 | | eleq2 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑓‘𝑧) ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})) |
| 30 | 28, 29 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = {(𝑓‘𝑧), 𝑧} → ((𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣) ↔ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧}))) |
| 31 | 30 | rspcev 3622 |
. . . . . . . . . . . . . . 15
⊢ (({(𝑓‘𝑧), 𝑧} ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ {(𝑓‘𝑧), 𝑧} ∧ (𝑓‘𝑧) ∈ {(𝑓‘𝑧), 𝑧})) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)) |
| 32 | 22, 27, 31 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)) |
| 33 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑧 ↔ (𝑓‘𝑧) ∈ 𝑧)) |
| 34 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝑓‘𝑧) → (𝑤 ∈ 𝑣 ↔ (𝑓‘𝑧) ∈ 𝑣)) |
| 35 | 34 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑓‘𝑧) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))) |
| 36 | 35 | rexbidv 3179 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑓‘𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣))) |
| 37 | 33, 36 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑓‘𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)))) |
| 38 | 25, 37 | spcev 3606 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘𝑧) ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ (𝑓‘𝑧) ∈ 𝑣)) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 39 | 32, 38 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘𝑧) ∈ 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 40 | 39 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑧) ∈ 𝑧 → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))) |
| 41 | 3, 40 | syl8 76 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))))) |
| 42 | 41 | impd 410 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))) |
| 43 | 42 | pm2.43d 53 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))) |
| 44 | | df-rex 3071 |
. . . . . . . . . . . . 13
⊢
(∃𝑣 ∈
{𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 45 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑣 ∈ V |
| 46 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑣 → (𝑔 = {(𝑓‘𝑢), 𝑢} ↔ 𝑣 = {(𝑓‘𝑢), 𝑢})) |
| 47 | 46 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑣 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}))) |
| 48 | 47 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑣 → (∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}))) |
| 49 | 45, 48 | elab 3679 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ↔ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢})) |
| 50 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑢 → (𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅)) |
| 51 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢)) |
| 52 | 51 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑧)) |
| 53 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑢 → ((𝑓‘𝑢) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢)) |
| 54 | 52, 53 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢)) |
| 55 | 50, 54 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑢 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢))) |
| 56 | 55 | rspccv 3619 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢))) |
| 57 | | elneq 9638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 ∈ 𝑧 → 𝑤 ≠ 𝑧) |
| 58 | 57 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 ∈ 𝑧 → ¬ 𝑤 = 𝑧) |
| 59 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑤 ∈ V |
| 60 | | neqne 2948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (¬
𝑤 = 𝑧 → 𝑤 ≠ 𝑧) |
| 61 | | prel12g 4864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤 ≠ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}))) |
| 62 | 59, 23, 60, 61 | mp3an12i 1467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (¬
𝑤 = 𝑧 → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}))) |
| 63 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ {(𝑓‘𝑢), 𝑢})) |
| 64 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ {(𝑓‘𝑢), 𝑢})) |
| 65 | 63, 64 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣) ↔ (𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}))) |
| 66 | | ancom 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣) ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) |
| 67 | 65, 66 | bitr3di 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑤 ∈ {(𝑓‘𝑢), 𝑢} ∧ 𝑧 ∈ {(𝑓‘𝑢), 𝑢}) ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 68 | 62, 67 | sylan9bbr 510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ ¬ 𝑤 = 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 69 | 58, 68 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ 𝑤 ∈ 𝑧) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 70 | 69 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑣 = {(𝑓‘𝑢), 𝑢} ∧ (𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢)) → ({𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢} ↔ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 71 | 70 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢}) ↔ ((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))) |
| 72 | 23 | preleq 9656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ {𝑤, 𝑧} = {(𝑓‘𝑢), 𝑢}) → (𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢)) |
| 73 | 71, 72 | biimtrrdi 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → (𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢))) |
| 74 | 51 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑢 → (𝑤 = (𝑓‘𝑧) ↔ 𝑤 = (𝑓‘𝑢))) |
| 75 | 74 | biimparc 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 = (𝑓‘𝑢) ∧ 𝑧 = 𝑢) → 𝑤 = (𝑓‘𝑧)) |
| 76 | 73, 75 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (((𝑤 ∈ 𝑧 ∧ (𝑓‘𝑢) ∈ 𝑢) ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧))) |
| 77 | 76 | exp4c 432 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = {(𝑓‘𝑢), 𝑢} → (𝑤 ∈ 𝑧 → ((𝑓‘𝑢) ∈ 𝑢 → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))) |
| 78 | 77 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓‘𝑢) ∈ 𝑢 → (𝑤 ∈ 𝑧 → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))) |
| 79 | 56, 78 | syl8 76 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑤 ∈ 𝑧 → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))))) |
| 80 | 79 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ 𝑧 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))))) |
| 81 | 80 | imp 406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑢 ∈ 𝑥 → (𝑢 ≠ ∅ → (𝑣 = {(𝑓‘𝑢), 𝑢} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))))) |
| 82 | 81 | imp4a 422 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))) |
| 83 | 82 | com3l 89 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))) |
| 84 | 83 | rexlimiv 3148 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢 ∈
𝑥 (𝑢 ≠ ∅ ∧ 𝑣 = {(𝑓‘𝑢), 𝑢}) → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))) |
| 85 | 49, 84 | sylbi 217 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑤 ∈ 𝑧 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧)))) |
| 86 | 85 | expd 415 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (𝑤 ∈ 𝑧 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))) |
| 87 | 86 | com13 88 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑤 ∈ 𝑧 → (𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))))) |
| 88 | 87 | imp4b 421 |
. . . . . . . . . . . . . 14
⊢
((∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → ((𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧))) |
| 89 | 88 | exlimdv 1933 |
. . . . . . . . . . . . 13
⊢
((∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → (∃𝑣(𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∧ (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧))) |
| 90 | 44, 89 | biimtrid 242 |
. . . . . . . . . . . 12
⊢
((∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ 𝑤 ∈ 𝑧) → (∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) → 𝑤 = (𝑓‘𝑧))) |
| 91 | 90 | expimpd 453 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧))) |
| 92 | 91 | alrimiv 1927 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧))) |
| 93 | | mo2icl 3720 |
. . . . . . . . . 10
⊢
(∀𝑤((𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → 𝑤 = (𝑓‘𝑧)) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 94 | 92, 93 | syl 17 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 95 | 43, 94 | jctird 526 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))))) |
| 96 | | df-reu 3381 |
. . . . . . . . 9
⊢
(∃!𝑤 ∈
𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 97 | | df-eu 2569 |
. . . . . . . . 9
⊢
(∃!𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))) |
| 98 | 96, 97 | bitri 275 |
. . . . . . . 8
⊢
(∃!𝑤 ∈
𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ (∃𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ∧ ∃*𝑤(𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))) |
| 99 | 95, 98 | imbitrrdi 252 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 100 | 99 | expd 415 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))) |
| 101 | 2, 100 | ralrimi 3257 |
. . . . 5
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 102 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
| 103 | 102 | rnex 7932 |
. . . . . . . . . 10
⊢ ran 𝑓 ∈ V |
| 104 | | p0ex 5384 |
. . . . . . . . . 10
⊢ {∅}
∈ V |
| 105 | 103, 104 | unex 7764 |
. . . . . . . . 9
⊢ (ran
𝑓 ∪ {∅}) ∈
V |
| 106 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 107 | 105, 106 | unex 7764 |
. . . . . . . 8
⊢ ((ran
𝑓 ∪ {∅}) ∪
𝑥) ∈
V |
| 108 | 107 | pwex 5380 |
. . . . . . 7
⊢ 𝒫
((ran 𝑓 ∪ {∅})
∪ 𝑥) ∈
V |
| 109 | | ssun1 4178 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑓 ∪ {∅}) ⊆
((ran 𝑓 ∪ {∅})
∪ 𝑥) |
| 110 | | fvrn0 6936 |
. . . . . . . . . . . . . 14
⊢ (𝑓‘𝑢) ∈ (ran 𝑓 ∪ {∅}) |
| 111 | 109, 110 | sselii 3980 |
. . . . . . . . . . . . 13
⊢ (𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) |
| 112 | | elun2 4183 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ 𝑥 → 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) |
| 113 | | prssi 4821 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘𝑢) ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ∧ 𝑢 ∈ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) |
| 114 | 111, 112,
113 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) |
| 115 | | prex 5437 |
. . . . . . . . . . . . 13
⊢ {(𝑓‘𝑢), 𝑢} ∈ V |
| 116 | 115 | elpw 4604 |
. . . . . . . . . . . 12
⊢ ({(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ⊆ ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) |
| 117 | 114, 116 | sylibr 234 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ 𝑥 → {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) |
| 118 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑔 = {(𝑓‘𝑢), 𝑢} → (𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) ↔ {(𝑓‘𝑢), 𝑢} ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))) |
| 119 | 117, 118 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝑥 → (𝑔 = {(𝑓‘𝑢), 𝑢} → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))) |
| 120 | 119 | adantld 490 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝑥 → ((𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥))) |
| 121 | 120 | rexlimiv 3148 |
. . . . . . . 8
⊢
(∃𝑢 ∈
𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢}) → 𝑔 ∈ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥)) |
| 122 | 121 | abssi 4070 |
. . . . . . 7
⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ⊆ 𝒫 ((ran 𝑓 ∪ {∅}) ∪ 𝑥) |
| 123 | 108, 122 | ssexi 5322 |
. . . . . 6
⊢ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} ∈ V |
| 124 | | rexeq 3322 |
. . . . . . . . 9
⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 125 | 124 | reubidv 3398 |
. . . . . . . 8
⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣) ↔ ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 126 | 125 | imbi2d 340 |
. . . . . . 7
⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → ((𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))) |
| 127 | 126 | ralbidv 3178 |
. . . . . 6
⊢ (𝑦 = {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))) |
| 128 | 123, 127 | spcev 3606 |
. . . . 5
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ {𝑔 ∣ ∃𝑢 ∈ 𝑥 (𝑢 ≠ ∅ ∧ 𝑔 = {(𝑓‘𝑢), 𝑢})} (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 129 | 101, 128 | syl 17 |
. . . 4
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 130 | 129 | exlimiv 1930 |
. . 3
⊢
(∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 131 | 130 | alimi 1811 |
. 2
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |
| 132 | 1, 131 | sylbi 217 |
1
⊢
(CHOICE → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))) |