This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( ( 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 ) )