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