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 ) |
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 ) |