mapsspm

Description: Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007) (Revised by Mario Carneiro, 27-Feb-2016)

		Ref	Expression
	Assertion	mapsspm	$⊢ A^{B} \subseteq A ↑_{𝑝𝑚} B$

Step	Hyp	Ref	Expression
1		elmapex	$⊢ f \in (A^{B}) \to (A \in V \land B \in V)$
2	1	simprd	$⊢ f \in (A^{B}) \to B \in V$
3	1	simpld	$⊢ f \in (A^{B}) \to A \in V$
4		elmapi	$⊢ f \in (A^{B}) \to f : B ⟶ A$
5		fpmg	$⊢ (B \in V \land A \in V \land f : B ⟶ A) \to f \in (A ↑_{𝑝𝑚} B)$
6	2 3 4 5	syl3anc	$⊢ f \in (A^{B}) \to f \in (A ↑_{𝑝𝑚} B)$
7	6	ssriv	$⊢ A^{B} \subseteq A ↑_{𝑝𝑚} B$

Metamath Proof Explorer