Metamath Proof Explorer

Theorem om2uzrani

Description: Range of G (see om2uz0i ). (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1 
|- C e. ZZ
om2uz.2 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
Assertion om2uzrani 
|- ran G = ( ZZ>= ` C )

Proof

Step Hyp Ref Expression
1 om2uz.1 
 |-  C e. ZZ
2 om2uz.2 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
3 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om ) Fn _om
4 2 fneq1i 
 |-  ( G Fn _om <-> ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om ) Fn _om )
5 3 4 mpbir 
 |-  G Fn _om
6 fvelrnb 
 |-  ( G Fn _om -> ( y e. ran G <-> E. z e. _om ( G ` z ) = y ) )
7 5 6 ax-mp 
 |-  ( y e. ran G <-> E. z e. _om ( G ` z ) = y )
8 1 2 om2uzuzi 
 |-  ( z e. _om -> ( G ` z ) e. ( ZZ>= ` C ) )
9 eleq1 
 |-  ( ( G ` z ) = y -> ( ( G ` z ) e. ( ZZ>= ` C ) <-> y e. ( ZZ>= ` C ) ) )
10 8 9 syl5ibcom 
 |-  ( z e. _om -> ( ( G ` z ) = y -> y e. ( ZZ>= ` C ) ) )
11 10 rexlimiv 
 |-  ( E. z e. _om ( G ` z ) = y -> y e. ( ZZ>= ` C ) )
12 7 11 sylbi 
 |-  ( y e. ran G -> y e. ( ZZ>= ` C ) )
13 eleq1 
 |-  ( z = C -> ( z e. ran G <-> C e. ran G ) )
14 eleq1 
 |-  ( z = y -> ( z e. ran G <-> y e. ran G ) )
15 eleq1 
 |-  ( z = ( y + 1 ) -> ( z e. ran G <-> ( y + 1 ) e. ran G ) )
16 1 2 om2uz0i 
 |-  ( G ` (/) ) = C
17 peano1 
 |-  (/) e. _om
18 fnfvelrn 
 |-  ( ( G Fn _om /\ (/) e. _om ) -> ( G ` (/) ) e. ran G )
19 5 17 18 mp2an 
 |-  ( G ` (/) ) e. ran G
20 16 19 eqeltrri 
 |-  C e. ran G
21 1 2 om2uzsuci 
 |-  ( z e. _om -> ( G ` suc z ) = ( ( G ` z ) + 1 ) )
22 oveq1 
 |-  ( ( G ` z ) = y -> ( ( G ` z ) + 1 ) = ( y + 1 ) )
23 21 22 sylan9eq 
 |-  ( ( z e. _om /\ ( G ` z ) = y ) -> ( G ` suc z ) = ( y + 1 ) )
24 peano2 
 |-  ( z e. _om -> suc z e. _om )
25 fnfvelrn 
 |-  ( ( G Fn _om /\ suc z e. _om ) -> ( G ` suc z ) e. ran G )
26 5 24 25 sylancr 
 |-  ( z e. _om -> ( G ` suc z ) e. ran G )
27 26 adantr 
 |-  ( ( z e. _om /\ ( G ` z ) = y ) -> ( G ` suc z ) e. ran G )
28 23 27 eqeltrrd 
 |-  ( ( z e. _om /\ ( G ` z ) = y ) -> ( y + 1 ) e. ran G )
29 28 rexlimiva 
 |-  ( E. z e. _om ( G ` z ) = y -> ( y + 1 ) e. ran G )
30 7 29 sylbi 
 |-  ( y e. ran G -> ( y + 1 ) e. ran G )
31 30 a1i 
 |-  ( y e. ( ZZ>= ` C ) -> ( y e. ran G -> ( y + 1 ) e. ran G ) )
32 13 14 15 14 20 31 uzind4i 
 |-  ( y e. ( ZZ>= ` C ) -> y e. ran G )
33 12 32 impbii 
 |-  ( y e. ran G <-> y e. ( ZZ>= ` C ) )
34 33 eqriv 
 |-  ran G = ( ZZ>= ` C )