Metamath Proof Explorer


Theorem wunsuc

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 )

Proof

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 )