This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmvalg

Description: The value of the partial mapping operation. ( A ^pm B ) is the set of all partial functions that map from B to A . (Contributed by NM, 15-Nov-2007) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion pmvalg ⊢ A ∈ C ∧ B ∈ D → A ↑ 𝑝𝑚 B = f ∈ 𝒫 B × A | Fun ⁡ f

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ f ∈ 𝒫 B × A | Fun ⁡ f ⊆ 𝒫 B × A
2 xpexg ⊢ B ∈ D ∧ A ∈ C → B × A ∈ V
3 2 ancoms ⊢ A ∈ C ∧ B ∈ D → B × A ∈ V
4 3 pwexd ⊢ A ∈ C ∧ B ∈ D → 𝒫 B × A ∈ V
5 ssexg ⊢ f ∈ 𝒫 B × A | Fun ⁡ f ⊆ 𝒫 B × A ∧ 𝒫 B × A ∈ V → f ∈ 𝒫 B × A | Fun ⁡ f ∈ V
6 1 4 5 sylancr ⊢ A ∈ C ∧ B ∈ D → f ∈ 𝒫 B × A | Fun ⁡ f ∈ V
7 elex ⊢ A ∈ C → A ∈ V
8 elex ⊢ B ∈ D → B ∈ V
9 xpeq2 ⊢ x = A → y × x = y × A
10 9 pweqd ⊢ x = A → 𝒫 y × x = 𝒫 y × A
11 10 rabeqdv ⊢ x = A → f ∈ 𝒫 y × x | Fun ⁡ f = f ∈ 𝒫 y × A | Fun ⁡ f
12 xpeq1 ⊢ y = B → y × A = B × A
13 12 pweqd ⊢ y = B → 𝒫 y × A = 𝒫 B × A
14 13 rabeqdv ⊢ y = B → f ∈ 𝒫 y × A | Fun ⁡ f = f ∈ 𝒫 B × A | Fun ⁡ f
15 df-pm ⊢ ↑ 𝑝𝑚 = x ∈ V , y ∈ V ⟼ f ∈ 𝒫 y × x | Fun ⁡ f
16 11 14 15 ovmpog ⊢ A ∈ V ∧ B ∈ V ∧ f ∈ 𝒫 B × A | Fun ⁡ f ∈ V → A ↑ 𝑝𝑚 B = f ∈ 𝒫 B × A | Fun ⁡ f
17 16 3expia ⊢ A ∈ V ∧ B ∈ V → f ∈ 𝒫 B × A | Fun ⁡ f ∈ V → A ↑ 𝑝𝑚 B = f ∈ 𝒫 B × A | Fun ⁡ f
18 7 8 17 syl2an ⊢ A ∈ C ∧ B ∈ D → f ∈ 𝒫 B × A | Fun ⁡ f ∈ V → A ↑ 𝑝𝑚 B = f ∈ 𝒫 B × A | Fun ⁡ f
19 6 18 mpd ⊢ A ∈ C ∧ B ∈ D → A ↑ 𝑝𝑚 B = f ∈ 𝒫 B × A | Fun ⁡ f