| Step | Hyp | Ref
| Expression |
| 1 | | df-ima 5698 |
. . 3
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} “ 𝒫 𝐵) = ran ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ↾ 𝒫 𝐵) |
| 2 | | relopab 5834 |
. . . . 5
⊢ Rel
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} |
| 3 | | dmopabss 5929 |
. . . . 5
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ⊆ 𝒫 𝐵 |
| 4 | | relssres 6040 |
. . . . 5
⊢ ((Rel
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ∧ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ⊆ 𝒫 𝐵) → ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ↾ 𝒫 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)}) |
| 5 | 2, 3, 4 | mp2an 692 |
. . . 4
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ↾ 𝒫 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} |
| 6 | 5 | rneqi 5948 |
. . 3
⊢ ran
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ↾ 𝒫 𝐵) = ran {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} |
| 7 | | rnopab 5965 |
. . . 4
⊢ ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} |
| 8 | | eleq1 2829 |
. . . . . . . . 9
⊢ ({𝑦} = 𝑥 → ({𝑦} ∈ 𝒫 𝐵 ↔ 𝑥 ∈ 𝒫 𝐵)) |
| 9 | 8 | biimparc 479 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥) → {𝑦} ∈ 𝒫 𝐵) |
| 10 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 11 | 10 | snelpw 5450 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↔ {𝑦} ∈ 𝒫 𝐵) |
| 12 | 9, 11 | sylibr 234 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥) → 𝑦 ∈ 𝐵) |
| 13 | 12 | exlimiv 1930 |
. . . . . 6
⊢
(∃𝑥(𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥) → 𝑦 ∈ 𝐵) |
| 14 | | snelpwi 5448 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → {𝑦} ∈ 𝒫 𝐵) |
| 15 | | eqid 2737 |
. . . . . . . 8
⊢ {𝑦} = {𝑦} |
| 16 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑥 = {𝑦} → ({𝑦} = 𝑥 ↔ {𝑦} = {𝑦})) |
| 17 | 16 | rspcev 3622 |
. . . . . . . 8
⊢ (({𝑦} ∈ 𝒫 𝐵 ∧ {𝑦} = {𝑦}) → ∃𝑥 ∈ 𝒫 𝐵{𝑦} = 𝑥) |
| 18 | 14, 15, 17 | sylancl 586 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝒫 𝐵{𝑦} = 𝑥) |
| 19 | | df-rex 3071 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝒫 𝐵{𝑦} = 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)) |
| 20 | 18, 19 | sylib 218 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 → ∃𝑥(𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)) |
| 21 | 13, 20 | impbii 209 |
. . . . 5
⊢
(∃𝑥(𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥) ↔ 𝑦 ∈ 𝐵) |
| 22 | 21 | abbii 2809 |
. . . 4
⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} = {𝑦 ∣ 𝑦 ∈ 𝐵} |
| 23 | | abid2 2879 |
. . . 4
⊢ {𝑦 ∣ 𝑦 ∈ 𝐵} = 𝐵 |
| 24 | 7, 22, 23 | 3eqtri 2769 |
. . 3
⊢ ran
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} = 𝐵 |
| 25 | 1, 6, 24 | 3eqtri 2769 |
. 2
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} “ 𝒫 𝐵) = 𝐵 |
| 26 | | funopab 6601 |
. . . 4
⊢ (Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)) |
| 27 | | mosneq 4842 |
. . . . 5
⊢
∃*𝑦{𝑦} = 𝑥 |
| 28 | 27 | moani 2553 |
. . . 4
⊢
∃*𝑦(𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥) |
| 29 | 26, 28 | mpgbir 1799 |
. . 3
⊢ Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} |
| 30 | | imafi 9353 |
. . 3
⊢ ((Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} ∧ 𝒫 𝐵 ∈ Fin) → ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} “ 𝒫 𝐵) ∈ Fin) |
| 31 | 29, 30 | mpan 690 |
. 2
⊢
(𝒫 𝐵 ∈
Fin → ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐵 ∧ {𝑦} = 𝑥)} “ 𝒫 𝐵) ∈ Fin) |
| 32 | 25, 31 | eqeltrrid 2846 |
1
⊢
(𝒫 𝐵 ∈
Fin → 𝐵 ∈
Fin) |