Theorem wunmap

Description: A weak universe is closed under 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	wunmap	$$⊢\phi \to A^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 2 3	wunpm	$$⊢\phi \to A{\uparrow }_{𝑝𝑚}B\in U$$
5		mapsspm	$$⊢A^B\subseteq A{\uparrow }_{𝑝𝑚}B$$
6	5	a1i	$$⊢\phi \to A^B\subseteq A{\uparrow }_{𝑝𝑚}B$$
7	1 4 6	wunss	$$⊢\phi \to A^B\in U$$