Metamath Proof Explorer

Theorem uzenom

Description: An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis uzinf.1 
|- Z = ( ZZ>= ` M )
Assertion uzenom 
|- ( M e. ZZ -> Z ~~ _om )

Proof

Step Hyp Ref Expression
1 uzinf.1 
 |-  Z = ( ZZ>= ` M )
2 fveq2 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> ( ZZ>= ` M ) = ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) )
3 1 2 eqtrid 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> Z = ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) )
4 3 breq1d 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> ( Z ~~ _om <-> ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ~~ _om ) )
5 omex 
 |-  _om e. _V
6 fvex 
 |-  ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) e. _V
7 0z 
 |-  0 e. ZZ
8 7 elimel 
 |-  if ( M e. ZZ , M , 0 ) e. ZZ
9 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( M e. ZZ , M , 0 ) ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( M e. ZZ , M , 0 ) ) |` _om )
10 8 9 om2uzf1oi 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( M e. ZZ , M , 0 ) ) |` _om ) : _om -1-1-onto-> ( ZZ>= ` if ( M e. ZZ , M , 0 ) )
11 f1oen2g 
 |-  ( ( _om e. _V /\ ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) e. _V /\ ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( M e. ZZ , M , 0 ) ) |` _om ) : _om -1-1-onto-> ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ) -> _om ~~ ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) )
12 5 6 10 11 mp3an 
 |-  _om ~~ ( ZZ>= ` if ( M e. ZZ , M , 0 ) )
13 12 ensymi 
 |-  ( ZZ>= ` if ( M e. ZZ , M , 0 ) ) ~~ _om
14 4 13 dedth 
 |-  ( M e. ZZ -> Z ~~ _om )