Metamath Proof Explorer

Theorem om2uzf1oi

Description: G (see om2uz0i ) is a one-to-one onto mapping. (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 om2uzf1oi 
|- G : _om -1-1-onto-> ( 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 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om ) Fn _om
4 2 fneq1i 
 |-  ( G Fn _om <-> ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om ) Fn _om )
5 3 4 mpbir 
 |-  G Fn _om
6 1 2 om2uzrani 
 |-  ran G = ( ZZ>= ` C )
7 6 eqimssi 
 |-  ran G C_ ( ZZ>= ` C )
8 df-f 
 |-  ( G : _om --> ( ZZ>= ` C ) <-> ( G Fn _om /\ ran G C_ ( ZZ>= ` C ) ) )
9 5 7 8 mpbir2an 
 |-  G : _om --> ( ZZ>= ` C )
10 1 2 om2uzuzi 
 |-  ( y e. _om -> ( G ` y ) e. ( ZZ>= ` C ) )
11 eluzelz 
 |-  ( ( G ` y ) e. ( ZZ>= ` C ) -> ( G ` y ) e. ZZ )
12 10 11 syl 
 |-  ( y e. _om -> ( G ` y ) e. ZZ )
13 12 zred 
 |-  ( y e. _om -> ( G ` y ) e. RR )
14 1 2 om2uzuzi 
 |-  ( z e. _om -> ( G ` z ) e. ( ZZ>= ` C ) )
15 eluzelz 
 |-  ( ( G ` z ) e. ( ZZ>= ` C ) -> ( G ` z ) e. ZZ )
16 14 15 syl 
 |-  ( z e. _om -> ( G ` z ) e. ZZ )
17 16 zred 
 |-  ( z e. _om -> ( G ` z ) e. RR )
18 lttri3 
 |-  ( ( ( G ` y ) e. RR /\ ( G ` z ) e. RR ) -> ( ( G ` y ) = ( G ` z ) <-> ( -. ( G ` y ) < ( G ` z ) /\ -. ( G ` z ) < ( G ` y ) ) ) )
19 13 17 18 syl2an 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( G ` y ) = ( G ` z ) <-> ( -. ( G ` y ) < ( G ` z ) /\ -. ( G ` z ) < ( G ` y ) ) ) )
20 ioran 
 |-  ( -. ( ( G ` y ) < ( G ` z ) \/ ( G ` z ) < ( G ` y ) ) <-> ( -. ( G ` y ) < ( G ` z ) /\ -. ( G ` z ) < ( G ` y ) ) )
21 19 20 bitr4di 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( G ` y ) = ( G ` z ) <-> -. ( ( G ` y ) < ( G ` z ) \/ ( G ` z ) < ( G ` y ) ) ) )
22 nnord 
 |-  ( y e. _om -> Ord y )
23 nnord 
 |-  ( z e. _om -> Ord z )
24 ordtri3 
 |-  ( ( Ord y /\ Ord z ) -> ( y = z <-> -. ( y e. z \/ z e. y ) ) )
25 22 23 24 syl2an 
 |-  ( ( y e. _om /\ z e. _om ) -> ( y = z <-> -. ( y e. z \/ z e. y ) ) )
26 25 con2bid 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( y e. z \/ z e. y ) <-> -. y = z ) )
27 1 2 om2uzlti 
 |-  ( ( y e. _om /\ z e. _om ) -> ( y e. z -> ( G ` y ) < ( G ` z ) ) )
28 1 2 om2uzlti 
 |-  ( ( z e. _om /\ y e. _om ) -> ( z e. y -> ( G ` z ) < ( G ` y ) ) )
29 28 ancoms 
 |-  ( ( y e. _om /\ z e. _om ) -> ( z e. y -> ( G ` z ) < ( G ` y ) ) )
30 27 29 orim12d 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( y e. z \/ z e. y ) -> ( ( G ` y ) < ( G ` z ) \/ ( G ` z ) < ( G ` y ) ) ) )
31 26 30 sylbird 
 |-  ( ( y e. _om /\ z e. _om ) -> ( -. y = z -> ( ( G ` y ) < ( G ` z ) \/ ( G ` z ) < ( G ` y ) ) ) )
32 31 con1d 
 |-  ( ( y e. _om /\ z e. _om ) -> ( -. ( ( G ` y ) < ( G ` z ) \/ ( G ` z ) < ( G ` y ) ) -> y = z ) )
33 21 32 sylbid 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) )
34 33 rgen2 
 |-  A. y e. _om A. z e. _om ( ( G ` y ) = ( G ` z ) -> y = z )
35 dff13 
 |-  ( G : _om -1-1-> ( ZZ>= ` C ) <-> ( G : _om --> ( ZZ>= ` C ) /\ A. y e. _om A. z e. _om ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
36 9 34 35 mpbir2an 
 |-  G : _om -1-1-> ( ZZ>= ` C )
37 dff1o5 
 |-  ( G : _om -1-1-onto-> ( ZZ>= ` C ) <-> ( G : _om -1-1-> ( ZZ>= ` C ) /\ ran G = ( ZZ>= ` C ) ) )
38 36 6 37 mpbir2an 
 |-  G : _om -1-1-onto-> ( ZZ>= ` C )