| Step | Hyp | Ref
| Expression |
| 1 | | fpwrelmap.3 |
. . 3
⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
| 2 | | fpwrelmap.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
| 3 | 2 | a1i 11 |
. . . . 5
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝐴 ∈ V) |
| 4 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ (𝑓‘𝑥)) |
| 5 | | elmapi 8889 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓:𝐴⟶𝒫 𝐵) |
| 6 | 5 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ 𝒫 𝐵) |
| 7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑓‘𝑥) ∈ 𝒫 𝐵) |
| 8 | | elelpwi 4610 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ∈ 𝒫 𝐵) → 𝑦 ∈ 𝐵) |
| 9 | 4, 7, 8 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵) |
| 10 | 9 | ex 412 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵)) |
| 11 | 10 | alrimiv 1927 |
. . . . . 6
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵)) |
| 12 | | abss 4063 |
. . . . . . 7
⊢ ({𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵)) |
| 13 | | fpwrelmap.2 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 14 | 13 | ssex 5321 |
. . . . . . 7
⊢ ({𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ⊆ 𝐵 → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V) |
| 15 | 12, 14 | sylbir 235 |
. . . . . 6
⊢
(∀𝑦(𝑦 ∈ (𝑓‘𝑥) → 𝑦 ∈ 𝐵) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V) |
| 16 | 11, 15 | syl 17 |
. . . . 5
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} ∈ V) |
| 17 | 3, 16 | opabex3d 7990 |
. . . 4
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V) |
| 18 | 17 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝑓
∈ (𝒫 𝐵
↑m 𝐴))
→ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ∈ V) |
| 19 | 2 | mptex 7243 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V |
| 20 | 19 | a1i 11 |
. . 3
⊢
((⊤ ∧ 𝑟
∈ 𝒫 (𝐴 ×
𝐵)) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) ∈ V) |
| 21 | 10 | imdistanda 571 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 22 | 21 | ssopab2dv 5556 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}) |
| 24 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
| 25 | | df-xp 5691 |
. . . . . . . . 9
⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
| 26 | 25 | a1i 11 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}) |
| 27 | 23, 24, 26 | 3sstr4d 4039 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ⊆ (𝐴 × 𝐵)) |
| 28 | | velpw 4605 |
. . . . . . 7
⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↔ 𝑟 ⊆ (𝐴 × 𝐵)) |
| 29 | 27, 28 | sylibr 234 |
. . . . . 6
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑟 ∈ 𝒫 (𝐴 × 𝐵)) |
| 30 | 5 | feqmptd 6977 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥))) |
| 31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥))) |
| 32 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) |
| 33 | | nfopab1 5213 |
. . . . . . . . . 10
⊢
Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} |
| 34 | 33 | nfeq2 2923 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} |
| 35 | 32, 34 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
| 36 | | df-rab 3437 |
. . . . . . . . . 10
⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)} |
| 37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)}) |
| 38 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) |
| 39 | | nfopab2 5214 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} |
| 40 | 39 | nfeq2 2923 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} |
| 41 | 38, 40 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
| 42 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑥 ∈ 𝐴 |
| 43 | 41, 42 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) |
| 44 | 9 | adantllr 719 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑦 ∈ 𝐵) |
| 45 | | df-br 5144 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥𝑟𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑟) |
| 46 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (〈𝑥, 𝑦〉 ∈ 𝑟 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) |
| 47 | | opabidw 5529 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))) |
| 48 | 46, 47 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (〈𝑥, 𝑦〉 ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))) |
| 49 | 45, 48 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))) |
| 50 | 49 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))) |
| 51 | | elfvdm 6943 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ dom 𝑓) |
| 52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ dom 𝑓) |
| 53 | 5 | fdmd 6746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → dom 𝑓 = 𝐴) |
| 54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → dom 𝑓 = 𝐴) |
| 55 | 52, 54 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥 ∈ 𝐴) |
| 56 | 55 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → 𝑥 ∈ 𝐴)) |
| 57 | 56 | pm4.71rd 562 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))) |
| 58 | 57 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))) |
| 59 | 50, 58 | bitr4d 282 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 ↔ 𝑦 ∈ (𝑓‘𝑥))) |
| 60 | 59 | biimpar 477 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦) |
| 61 | 44, 60 | jca 511 |
. . . . . . . . . . . 12
⊢ ((((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)) |
| 62 | 61 | ex 412 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) → (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))) |
| 63 | 59 | biimpd 229 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑥𝑟𝑦 → 𝑦 ∈ (𝑓‘𝑥))) |
| 64 | 63 | adantld 490 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥))) |
| 65 | 62, 64 | impbid 212 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))) |
| 66 | 43, 65 | abbid 2810 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)}) |
| 67 | | abid2 2879 |
. . . . . . . . . 10
⊢ {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥) |
| 68 | 67 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝑦 ∈ (𝑓‘𝑥)} = (𝑓‘𝑥)) |
| 69 | 37, 66, 68 | 3eqtr2rd 2784 |
. . . . . . . 8
⊢ (((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 70 | 35, 69 | mpteq2da 5240 |
. . . . . . 7
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑥 ∈ 𝐴 ↦ (𝑓‘𝑥)) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
| 71 | 31, 70 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
| 72 | 29, 71 | jca 511 |
. . . . 5
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) |
| 73 | | ssrab2 4080 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ⊆ 𝐵 |
| 74 | 13, 73 | elpwi2 5335 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵 |
| 75 | 74 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥 ∈ 𝐴) → {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ 𝒫 𝐵) |
| 76 | 75 | fmpttd 7135 |
. . . . . . . . 9
⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵) |
| 77 | 76 | adantr 480 |
. . . . . . . 8
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵) |
| 78 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
| 79 | 78 | feq1d 6720 |
. . . . . . . 8
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓:𝐴⟶𝒫 𝐵 ↔ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}):𝐴⟶𝒫 𝐵)) |
| 80 | 77, 79 | mpbird 257 |
. . . . . . 7
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓:𝐴⟶𝒫 𝐵) |
| 81 | 13 | pwex 5380 |
. . . . . . . 8
⊢ 𝒫
𝐵 ∈ V |
| 82 | 81, 2 | elmap 8911 |
. . . . . . 7
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵) |
| 83 | 80, 82 | sylibr 234 |
. . . . . 6
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑓 ∈ (𝒫 𝐵 ↑m 𝐴)) |
| 84 | | elpwi 4607 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) → 𝑟 ⊆ (𝐴 × 𝐵)) |
| 85 | 84 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (𝐴 × 𝐵)) |
| 86 | | xpss 5701 |
. . . . . . . . 9
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
| 87 | 85, 86 | sstrdi 3996 |
. . . . . . . 8
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 ⊆ (V × V)) |
| 88 | | df-rel 5692 |
. . . . . . . 8
⊢ (Rel
𝑟 ↔ 𝑟 ⊆ (V × V)) |
| 89 | 87, 88 | sylibr 234 |
. . . . . . 7
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel 𝑟) |
| 90 | | relopabv 5831 |
. . . . . . . 8
⊢ Rel
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))} |
| 91 | 90 | a1i 11 |
. . . . . . 7
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → Rel {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
| 92 | | id 22 |
. . . . . . 7
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) |
| 93 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑟 ∈ 𝒫 (𝐴 × 𝐵) |
| 94 | | nfmpt1 5250 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 95 | 94 | nfeq2 2923 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 96 | 93, 95 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
| 97 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑦 𝑟 ∈ 𝒫 (𝐴 × 𝐵) |
| 98 | 42 | nfci 2893 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝐴 |
| 99 | | nfrab1 3457 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} |
| 100 | 98, 99 | nfmpt 5249 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 101 | 100 | nfeq2 2923 |
. . . . . . . . 9
⊢
Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 102 | 97, 101 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
| 103 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑟 |
| 104 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑦𝑟 |
| 105 | | brelg 32621 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 106 | 84, 105 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 107 | 106 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 108 | 107 | simpld 494 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥 ∈ 𝐴) |
| 109 | 107 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ 𝐵) |
| 110 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑥𝑟𝑦) |
| 111 | 78 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓‘𝑥) = ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥)) |
| 112 | 13 | rabex 5339 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V |
| 113 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 114 | 113 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ∈ V) → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 115 | 112, 114 | mpan2 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 116 | 111, 115 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) = {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}) |
| 117 | 116 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) |
| 118 | | rabid 3458 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦} ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦)) |
| 119 | 117, 118 | bitrdi 287 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))) |
| 120 | 108, 119 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑦 ∈ (𝑓‘𝑥) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥𝑟𝑦))) |
| 121 | 109, 110,
120 | mpbir2and 713 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → 𝑦 ∈ (𝑓‘𝑥)) |
| 122 | 108, 121 | jca 511 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥𝑟𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))) |
| 123 | 122 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))) |
| 124 | 119 | simplbda 499 |
. . . . . . . . . . . 12
⊢ ((((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦) |
| 125 | 124 | expl 457 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)) → 𝑥𝑟𝑦)) |
| 126 | 123, 125 | impbid 212 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑥𝑟𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))) |
| 127 | 45, 126 | bitr3id 285 |
. . . . . . . . 9
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (〈𝑥, 𝑦〉 ∈ 𝑟 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥)))) |
| 128 | 127, 47 | bitr4di 289 |
. . . . . . . 8
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (〈𝑥, 𝑦〉 ∈ 𝑟 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) |
| 129 | 96, 102, 103, 104, 33, 39, 128 | eqrelrd2 32628 |
. . . . . . 7
⊢ (((Rel
𝑟 ∧ Rel {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ∧ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) → 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
| 130 | 89, 91, 92, 129 | syl21anc 838 |
. . . . . 6
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) |
| 131 | 83, 130 | jca 511 |
. . . . 5
⊢ ((𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})) → (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})) |
| 132 | 72, 131 | impbii 209 |
. . . 4
⊢ ((𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ∧ 𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦}))) |
| 133 | 132 | a1i 11 |
. . 3
⊢ (⊤
→ ((𝑓 ∈
(𝒫 𝐵
↑m 𝐴) ∧
𝑟 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ↔ (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ {𝑦 ∈ 𝐵 ∣ 𝑥𝑟𝑦})))) |
| 134 | 1, 18, 20, 133 | f1od 7685 |
. 2
⊢ (⊤
→ 𝑀:(𝒫 𝐵 ↑m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)) |
| 135 | 134 | mptru 1547 |
1
⊢ 𝑀:(𝒫 𝐵 ↑m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵) |