Metamath Proof Explorer

Theorem om2uzuzi

Description: The value G (see om2uz0i ) at an ordinal natural number is in the upper integers. (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 om2uzuzi 
|- ( A e. _om -> ( G ` A ) e. ( 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 fveq2 
 |-  ( y = (/) -> ( G ` y ) = ( G ` (/) ) )
4 3 eleq1d 
 |-  ( y = (/) -> ( ( G ` y ) e. ( ZZ>= ` C ) <-> ( G ` (/) ) e. ( ZZ>= ` C ) ) )
5 fveq2 
 |-  ( y = z -> ( G ` y ) = ( G ` z ) )
6 5 eleq1d 
 |-  ( y = z -> ( ( G ` y ) e. ( ZZ>= ` C ) <-> ( G ` z ) e. ( ZZ>= ` C ) ) )
7 fveq2 
 |-  ( y = suc z -> ( G ` y ) = ( G ` suc z ) )
8 7 eleq1d 
 |-  ( y = suc z -> ( ( G ` y ) e. ( ZZ>= ` C ) <-> ( G ` suc z ) e. ( ZZ>= ` C ) ) )
9 fveq2 
 |-  ( y = A -> ( G ` y ) = ( G ` A ) )
10 9 eleq1d 
 |-  ( y = A -> ( ( G ` y ) e. ( ZZ>= ` C ) <-> ( G ` A ) e. ( ZZ>= ` C ) ) )
11 1 2 om2uz0i 
 |-  ( G ` (/) ) = C
12 uzid 
 |-  ( C e. ZZ -> C e. ( ZZ>= ` C ) )
13 1 12 ax-mp 
 |-  C e. ( ZZ>= ` C )
14 11 13 eqeltri 
 |-  ( G ` (/) ) e. ( ZZ>= ` C )
15 peano2uz 
 |-  ( ( G ` z ) e. ( ZZ>= ` C ) -> ( ( G ` z ) + 1 ) e. ( ZZ>= ` C ) )
16 1 2 om2uzsuci 
 |-  ( z e. _om -> ( G ` suc z ) = ( ( G ` z ) + 1 ) )
17 16 eleq1d 
 |-  ( z e. _om -> ( ( G ` suc z ) e. ( ZZ>= ` C ) <-> ( ( G ` z ) + 1 ) e. ( ZZ>= ` C ) ) )
18 15 17 imbitrrid 
 |-  ( z e. _om -> ( ( G ` z ) e. ( ZZ>= ` C ) -> ( G ` suc z ) e. ( ZZ>= ` C ) ) )
19 4 6 8 10 14 18 finds 
 |-  ( A e. _om -> ( G ` A ) e. ( ZZ>= ` C ) )