pmsspw

Description: Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Assertion	pmsspw	$⊢ A ↑_{𝑝𝑚} B \subseteq 𝒫 (B \times A)$

Step	Hyp	Ref	Expression
1		n0i	$⊢ f \in (A ↑_{𝑝𝑚} B) \to \neg A ↑_{𝑝𝑚} B = \emptyset$
2		fnpm	$⊢ ↑_{𝑝𝑚} Fn (V \times V)$
3	2	fndmi	$⊢ dom ↑_{𝑝𝑚} = V \times V$
4	3	ndmov	$⊢ \neg (A \in V \land B \in V) \to A ↑_{𝑝𝑚} B = \emptyset$
5	1 4	nsyl2	$⊢ f \in (A ↑_{𝑝𝑚} B) \to (A \in V \land B \in V)$
6		elpmg	$⊢ (A \in V \land B \in V) \to (f \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun f \land f \subseteq B \times A))$
7	5 6	syl	$⊢ f \in (A ↑_{𝑝𝑚} B) \to (f \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun f \land f \subseteq B \times A))$
8	7	ibi	$⊢ f \in (A ↑_{𝑝𝑚} B) \to (Fun f \land f \subseteq B \times A)$
9	8	simprd	$⊢ f \in (A ↑_{𝑝𝑚} B) \to f \subseteq B \times A$
10		velpw	$⊢ f \in 𝒫 (B \times A) \leftrightarrow f \subseteq B \times A$
11	9 10	sylibr	$⊢ f \in (A ↑_{𝑝𝑚} B) \to f \in 𝒫 (B \times A)$
12	11	ssriv	$⊢ A ↑_{𝑝𝑚} B \subseteq 𝒫 (B \times A)$

Metamath Proof Explorer