Theorem wunf

Description: A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wun0.1	|- ( ph -> U e. WUni )
	wunop.2	|- ( ph -> A e. U )
	wunop.3	|- ( ph -> B e. U )
	wunf.3	|- ( ph -> F : A --> B )
Assertion	wunf	|- ( ph -> F e. U )

Proof

Step	Hyp	Ref	Expression
1		wun0.1	|- ( ph -> U e. WUni )
2		wunop.2	|- ( ph -> A e. U )
3		wunop.3	|- ( ph -> B e. U )
4		wunf.3	|- ( ph -> F : A --> B )
5	1 3 2	wunmap	|- ( ph -> ( B ^m A ) e. U )
6	1 5	wunelss	|- ( ph -> ( B ^m A ) C_ U )
7	3 2	elmapd	|- ( ph -> ( F e. ( B ^m A ) <-> F : A --> B ) )
8	4 7	mpbird	|- ( ph -> F e. ( B ^m A ) )
9	6 8	sseldd	|- ( ph -> F e. U )