Step | Hyp | Ref
| Expression |
1 | | ssrab2 3650 |
. . 3
⊢ {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓} ⊆ 𝒫 (𝐵 × 𝐴) |
2 | | xpexg 6858 |
. . . . 5
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐴 ∈ 𝐶) → (𝐵 × 𝐴) ∈ V) |
3 | 2 | ancoms 468 |
. . . 4
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐵 × 𝐴) ∈ V) |
4 | | pwexg 4776 |
. . . 4
⊢ ((𝐵 × 𝐴) ∈ V → 𝒫 (𝐵 × 𝐴) ∈ V) |
5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝒫 (𝐵 × 𝐴) ∈ V) |
6 | | ssexg 4732 |
. . 3
⊢ (({𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓} ⊆ 𝒫 (𝐵 × 𝐴) ∧ 𝒫 (𝐵 × 𝐴) ∈ V) → {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓} ∈ V) |
7 | 1, 5, 6 | sylancr 694 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓} ∈ V) |
8 | | elex 3185 |
. . 3
⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) |
9 | | elex 3185 |
. . 3
⊢ (𝐵 ∈ 𝐷 → 𝐵 ∈ V) |
10 | | xpeq2 5053 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑦 × 𝑥) = (𝑦 × 𝐴)) |
11 | 10 | pweqd 4113 |
. . . . . 6
⊢ (𝑥 = 𝐴 → 𝒫 (𝑦 × 𝑥) = 𝒫 (𝑦 × 𝐴)) |
12 | | rabeq 3166 |
. . . . . 6
⊢
(𝒫 (𝑦
× 𝑥) = 𝒫
(𝑦 × 𝐴) → {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓} = {𝑓 ∈ 𝒫 (𝑦 × 𝐴) ∣ Fun 𝑓}) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝑥 = 𝐴 → {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓} = {𝑓 ∈ 𝒫 (𝑦 × 𝐴) ∣ Fun 𝑓}) |
14 | | xpeq1 5052 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 × 𝐴) = (𝐵 × 𝐴)) |
15 | 14 | pweqd 4113 |
. . . . . 6
⊢ (𝑦 = 𝐵 → 𝒫 (𝑦 × 𝐴) = 𝒫 (𝐵 × 𝐴)) |
16 | | rabeq 3166 |
. . . . . 6
⊢
(𝒫 (𝑦
× 𝐴) = 𝒫
(𝐵 × 𝐴) → {𝑓 ∈ 𝒫 (𝑦 × 𝐴) ∣ Fun 𝑓} = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓}) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝐵 → {𝑓 ∈ 𝒫 (𝑦 × 𝐴) ∣ Fun 𝑓} = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓}) |
18 | | df-pm 7747 |
. . . . 5
⊢
↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) |
19 | 13, 17, 18 | ovmpt2g 6693 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓} ∈ V) → (𝐴 ↑pm 𝐵) = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓}) |
20 | 19 | 3expia 1259 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ({𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓} ∈ V → (𝐴 ↑pm 𝐵) = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓})) |
21 | 8, 9, 20 | syl2an 493 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓} ∈ V → (𝐴 ↑pm 𝐵) = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓})) |
22 | 7, 21 | mpd 15 |
1
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑pm 𝐵) = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓}) |