Metamath Proof Explorer


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 )