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