Metamath Proof Explorer

Theorem om2uzlti

Description: Less-than relation for G (see om2uz0i ). (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 om2uzlti 
|- ( ( A e. _om /\ B e. _om ) -> ( A e. B -> ( G ` A ) < ( G ` B ) ) )

Proof

Step Hyp Ref Expression
1 om2uz.1 
 |-  C e. ZZ
2 om2uz.2 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
3 eleq2 
 |-  ( z = (/) -> ( A e. z <-> A e. (/) ) )
4 fveq2 
 |-  ( z = (/) -> ( G ` z ) = ( G ` (/) ) )
5 4 breq2d 
 |-  ( z = (/) -> ( ( G ` A ) < ( G ` z ) <-> ( G ` A ) < ( G ` (/) ) ) )
6 3 5 imbi12d 
 |-  ( z = (/) -> ( ( A e. z -> ( G ` A ) < ( G ` z ) ) <-> ( A e. (/) -> ( G ` A ) < ( G ` (/) ) ) ) )
7 6 imbi2d 
 |-  ( z = (/) -> ( ( A e. _om -> ( A e. z -> ( G ` A ) < ( G ` z ) ) ) <-> ( A e. _om -> ( A e. (/) -> ( G ` A ) < ( G ` (/) ) ) ) ) )
8 eleq2 
 |-  ( z = y -> ( A e. z <-> A e. y ) )
9 fveq2 
 |-  ( z = y -> ( G ` z ) = ( G ` y ) )
10 9 breq2d 
 |-  ( z = y -> ( ( G ` A ) < ( G ` z ) <-> ( G ` A ) < ( G ` y ) ) )
11 8 10 imbi12d 
 |-  ( z = y -> ( ( A e. z -> ( G ` A ) < ( G ` z ) ) <-> ( A e. y -> ( G ` A ) < ( G ` y ) ) ) )
12 11 imbi2d 
 |-  ( z = y -> ( ( A e. _om -> ( A e. z -> ( G ` A ) < ( G ` z ) ) ) <-> ( A e. _om -> ( A e. y -> ( G ` A ) < ( G ` y ) ) ) ) )
13 eleq2 
 |-  ( z = suc y -> ( A e. z <-> A e. suc y ) )
14 fveq2 
 |-  ( z = suc y -> ( G ` z ) = ( G ` suc y ) )
15 14 breq2d 
 |-  ( z = suc y -> ( ( G ` A ) < ( G ` z ) <-> ( G ` A ) < ( G ` suc y ) ) )
16 13 15 imbi12d 
 |-  ( z = suc y -> ( ( A e. z -> ( G ` A ) < ( G ` z ) ) <-> ( A e. suc y -> ( G ` A ) < ( G ` suc y ) ) ) )
17 16 imbi2d 
 |-  ( z = suc y -> ( ( A e. _om -> ( A e. z -> ( G ` A ) < ( G ` z ) ) ) <-> ( A e. _om -> ( A e. suc y -> ( G ` A ) < ( G ` suc y ) ) ) ) )
18 eleq2 
 |-  ( z = B -> ( A e. z <-> A e. B ) )
19 fveq2 
 |-  ( z = B -> ( G ` z ) = ( G ` B ) )
20 19 breq2d 
 |-  ( z = B -> ( ( G ` A ) < ( G ` z ) <-> ( G ` A ) < ( G ` B ) ) )
21 18 20 imbi12d 
 |-  ( z = B -> ( ( A e. z -> ( G ` A ) < ( G ` z ) ) <-> ( A e. B -> ( G ` A ) < ( G ` B ) ) ) )
22 21 imbi2d 
 |-  ( z = B -> ( ( A e. _om -> ( A e. z -> ( G ` A ) < ( G ` z ) ) ) <-> ( A e. _om -> ( A e. B -> ( G ` A ) < ( G ` B ) ) ) ) )
23 noel 
 |-  -. A e. (/)
24 23 pm2.21i 
 |-  ( A e. (/) -> ( G ` A ) < ( G ` (/) ) )
25 24 a1i 
 |-  ( A e. _om -> ( A e. (/) -> ( G ` A ) < ( G ` (/) ) ) )
26 id 
 |-  ( ( A e. y -> ( G ` A ) < ( G ` y ) ) -> ( A e. y -> ( G ` A ) < ( G ` y ) ) )
27 fveq2 
 |-  ( A = y -> ( G ` A ) = ( G ` y ) )
28 27 a1i 
 |-  ( ( A e. y -> ( G ` A ) < ( G ` y ) ) -> ( A = y -> ( G ` A ) = ( G ` y ) ) )
29 26 28 orim12d 
 |-  ( ( A e. y -> ( G ` A ) < ( G ` y ) ) -> ( ( A e. y \/ A = y ) -> ( ( G ` A ) < ( G ` y ) \/ ( G ` A ) = ( G ` y ) ) ) )
30 elsuc2g 
 |-  ( y e. _om -> ( A e. suc y <-> ( A e. y \/ A = y ) ) )
31 30 bicomd 
 |-  ( y e. _om -> ( ( A e. y \/ A = y ) <-> A e. suc y ) )
32 31 adantl 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A e. y \/ A = y ) <-> A e. suc y ) )
33 1 2 om2uzsuci 
 |-  ( y e. _om -> ( G ` suc y ) = ( ( G ` y ) + 1 ) )
34 33 breq2d 
 |-  ( y e. _om -> ( ( G ` A ) < ( G ` suc y ) <-> ( G ` A ) < ( ( G ` y ) + 1 ) ) )
35 34 adantl 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( G ` A ) < ( G ` suc y ) <-> ( G ` A ) < ( ( G ` y ) + 1 ) ) )
36 1 2 om2uzuzi 
 |-  ( A e. _om -> ( G ` A ) e. ( ZZ>= ` C ) )
37 1 2 om2uzuzi 
 |-  ( y e. _om -> ( G ` y ) e. ( ZZ>= ` C ) )
38 eluzelz 
 |-  ( ( G ` A ) e. ( ZZ>= ` C ) -> ( G ` A ) e. ZZ )
39 eluzelz 
 |-  ( ( G ` y ) e. ( ZZ>= ` C ) -> ( G ` y ) e. ZZ )
40 zleltp1 
 |-  ( ( ( G ` A ) e. ZZ /\ ( G ` y ) e. ZZ ) -> ( ( G ` A ) <_ ( G ` y ) <-> ( G ` A ) < ( ( G ` y ) + 1 ) ) )
41 38 39 40 syl2an 
 |-  ( ( ( G ` A ) e. ( ZZ>= ` C ) /\ ( G ` y ) e. ( ZZ>= ` C ) ) -> ( ( G ` A ) <_ ( G ` y ) <-> ( G ` A ) < ( ( G ` y ) + 1 ) ) )
42 36 37 41 syl2an 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( G ` A ) <_ ( G ` y ) <-> ( G ` A ) < ( ( G ` y ) + 1 ) ) )
43 36 38 syl 
 |-  ( A e. _om -> ( G ` A ) e. ZZ )
44 43 zred 
 |-  ( A e. _om -> ( G ` A ) e. RR )
45 37 39 syl 
 |-  ( y e. _om -> ( G ` y ) e. ZZ )
46 45 zred 
 |-  ( y e. _om -> ( G ` y ) e. RR )
47 leloe 
 |-  ( ( ( G ` A ) e. RR /\ ( G ` y ) e. RR ) -> ( ( G ` A ) <_ ( G ` y ) <-> ( ( G ` A ) < ( G ` y ) \/ ( G ` A ) = ( G ` y ) ) ) )
48 44 46 47 syl2an 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( G ` A ) <_ ( G ` y ) <-> ( ( G ` A ) < ( G ` y ) \/ ( G ` A ) = ( G ` y ) ) ) )
49 35 42 48 3bitr2rd 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( ( G ` A ) < ( G ` y ) \/ ( G ` A ) = ( G ` y ) ) <-> ( G ` A ) < ( G ` suc y ) ) )
50 32 49 imbi12d 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( ( A e. y \/ A = y ) -> ( ( G ` A ) < ( G ` y ) \/ ( G ` A ) = ( G ` y ) ) ) <-> ( A e. suc y -> ( G ` A ) < ( G ` suc y ) ) ) )
51 29 50 imbitrid 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A e. y -> ( G ` A ) < ( G ` y ) ) -> ( A e. suc y -> ( G ` A ) < ( G ` suc y ) ) ) )
52 51 expcom 
 |-  ( y e. _om -> ( A e. _om -> ( ( A e. y -> ( G ` A ) < ( G ` y ) ) -> ( A e. suc y -> ( G ` A ) < ( G ` suc y ) ) ) ) )
53 52 a2d 
 |-  ( y e. _om -> ( ( A e. _om -> ( A e. y -> ( G ` A ) < ( G ` y ) ) ) -> ( A e. _om -> ( A e. suc y -> ( G ` A ) < ( G ` suc y ) ) ) ) )
54 7 12 17 22 25 53 finds 
 |-  ( B e. _om -> ( A e. _om -> ( A e. B -> ( G ` A ) < ( G ` B ) ) ) )
55 54 impcom 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B -> ( G ` A ) < ( G ` B ) ) )