Theorem wunpm

Description: A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunop.2	$$⊢\phi \to A\in U$$
	wunop.3	$$⊢\phi \to B\in U$$
Assertion	wunpm	$$⊢\phi \to A{\uparrow }_{𝑝𝑚}B\in U$$

Proof

Step	Hyp	Ref	Expression
1		wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wunop.2	$$⊢\phi \to A\in U$$
3		wunop.3	$$⊢\phi \to B\in U$$
4	1 3 2	wunxp	$$⊢\phi \to B\times A\in U$$
5	1 4	wunpw	$$⊢\phi \to 𝒫\left(B\times A\right)\in U$$
6		pmsspw	$$⊢A{\uparrow }_{𝑝𝑚}B\subseteq 𝒫\left(B\times A\right)$$
7	6	a1i	$$⊢\phi \to A{\uparrow }_{𝑝𝑚}B\subseteq 𝒫\left(B\times A\right)$$
8	1 5 7	wunss	$$⊢\phi \to A{\uparrow }_{𝑝𝑚}B\in U$$