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 \in C \land B \in D) \to A ↑_{𝑝𝑚} B = \{f \in 𝒫 (B \times A) \| Fun f\}$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$⊢ \{f \in 𝒫 (B \times A) \| Fun f\} \subseteq 𝒫 (B \times A)$
2		xpexg	$⊢ (B \in D \land A \in C) \to B \times A \in V$
3	2	ancoms	$⊢ (A \in C \land B \in D) \to B \times A \in V$
4	3	pwexd	$⊢ (A \in C \land B \in D) \to 𝒫 (B \times A) \in V$
5		ssexg	$⊢ (\{f \in 𝒫 (B \times A) \| Fun f\} \subseteq 𝒫 (B \times A) \land 𝒫 (B \times A) \in V) \to \{f \in 𝒫 (B \times A) \| Fun f\} \in V$
6	1 4 5	sylancr	$⊢ (A \in C \land B \in D) \to \{f \in 𝒫 (B \times A) \| Fun f\} \in V$
7		elex	$⊢ A \in C \to A \in V$
8		elex	$⊢ B \in D \to B \in V$
9		xpeq2	$⊢ x = A \to y \times x = y \times A$
10	9	pweqd	$⊢ x = A \to 𝒫 (y \times x) = 𝒫 (y \times A)$
11	10	rabeqdv	$⊢ x = A \to \{f \in 𝒫 (y \times x) \| Fun f\} = \{f \in 𝒫 (y \times A) \| Fun f\}$
12		xpeq1	$⊢ y = B \to y \times A = B \times A$
13	12	pweqd	$⊢ y = B \to 𝒫 (y \times A) = 𝒫 (B \times A)$
14	13	rabeqdv	$⊢ y = B \to \{f \in 𝒫 (y \times A) \| Fun f\} = \{f \in 𝒫 (B \times A) \| Fun f\}$
15		df-pm	$⊢ ↑_{𝑝𝑚} = (x \in V, y \in V ⟼ \{f \in 𝒫 (y \times x) \| Fun f\})$
16	11 14 15	ovmpog	$⊢ (A \in V \land B \in V \land \{f \in 𝒫 (B \times A) \| Fun f\} \in V) \to A ↑_{𝑝𝑚} B = \{f \in 𝒫 (B \times A) \| Fun f\}$
17	16	3expia	$⊢ (A \in V \land B \in V) \to (\{f \in 𝒫 (B \times A) \| Fun f\} \in V \to A ↑_{𝑝𝑚} B = \{f \in 𝒫 (B \times A) \| Fun f\})$
18	7 8 17	syl2an	$⊢ (A \in C \land B \in D) \to (\{f \in 𝒫 (B \times A) \| Fun f\} \in V \to A ↑_{𝑝𝑚} B = \{f \in 𝒫 (B \times A) \| Fun f\})$
19	6 18	mpd	$⊢ (A \in C \land B \in D) \to A ↑_{𝑝𝑚} B = \{f \in 𝒫 (B \times A) \| Fun f\}$