Description: A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wununi.1 | |- ( ph -> U e. WUni ) |
|
wununi.2 | |- ( ph -> A e. U ) |
||
Assertion | wunsuc | |- ( ph -> suc A e. U ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wununi.1 | |- ( ph -> U e. WUni ) |
|
2 | wununi.2 | |- ( ph -> A e. U ) |
|
3 | df-suc | |- suc A = ( A u. { A } ) |
|
4 | 1 2 | wunsn | |- ( ph -> { A } e. U ) |
5 | 1 2 4 | wunun | |- ( ph -> ( A u. { A } ) e. U ) |
6 | 3 5 | eqeltrid | |- ( ph -> suc A e. U ) |