Metamath Proof Explorer

Theorem uzn0

Description: The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014)

Ref Expression
Assertion uzn0 
|- ( M e. ran ZZ>= -> M =/= (/) )

Proof

Step Hyp Ref Expression
1 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
2 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
3 fvelrnb 
 |-  ( ZZ>= Fn ZZ -> ( M e. ran ZZ>= <-> E. k e. ZZ ( ZZ>= ` k ) = M ) )
4 1 2 3 mp2b 
 |-  ( M e. ran ZZ>= <-> E. k e. ZZ ( ZZ>= ` k ) = M )
5 uzid 
 |-  ( k e. ZZ -> k e. ( ZZ>= ` k ) )
6 5 ne0d 
 |-  ( k e. ZZ -> ( ZZ>= ` k ) =/= (/) )
7 neeq1 
 |-  ( ( ZZ>= ` k ) = M -> ( ( ZZ>= ` k ) =/= (/) <-> M =/= (/) ) )
8 6 7 syl5ibcom 
 |-  ( k e. ZZ -> ( ( ZZ>= ` k ) = M -> M =/= (/) ) )
9 8 rexlimiv 
 |-  ( E. k e. ZZ ( ZZ>= ` k ) = M -> M =/= (/) )
10 4 9 sylbi 
 |-  ( M e. ran ZZ>= -> M =/= (/) )