Metamath Proof Explorer


Theorem om2uzisoi

Description: G (see om2uz0i ) is an isomorphism from natural ordinals to upper integers. (Contributed by NM, 9-Oct-2008) (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 om2uzisoi
|- G Isom _E , < ( _om , ( 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 1 2 om2uzf1oi
 |-  G : _om -1-1-onto-> ( ZZ>= ` C )
4 epel
 |-  ( y _E z <-> y e. z )
5 1 2 om2uzlt2i
 |-  ( ( y e. _om /\ z e. _om ) -> ( y e. z <-> ( G ` y ) < ( G ` z ) ) )
6 4 5 syl5bb
 |-  ( ( y e. _om /\ z e. _om ) -> ( y _E z <-> ( G ` y ) < ( G ` z ) ) )
7 6 rgen2
 |-  A. y e. _om A. z e. _om ( y _E z <-> ( G ` y ) < ( G ` z ) )
8 df-isom
 |-  ( G Isom _E , < ( _om , ( ZZ>= ` C ) ) <-> ( G : _om -1-1-onto-> ( ZZ>= ` C ) /\ A. y e. _om A. z e. _om ( y _E z <-> ( G ` y ) < ( G ` z ) ) ) )
9 3 7 8 mpbir2an
 |-  G Isom _E , < ( _om , ( ZZ>= ` C ) )