Metamath Proof Explorer


Theorem nnaordi

Description: Ordering property of addition. Proposition 8.4 of TakeutiZaring p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnaordi
|- ( ( B e. _om /\ C e. _om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )

Proof

Step Hyp Ref Expression
1 elnn
 |-  ( ( A e. B /\ B e. _om ) -> A e. _om )
2 1 ancoms
 |-  ( ( B e. _om /\ A e. B ) -> A e. _om )
3 2 adantll
 |-  ( ( ( C e. _om /\ B e. _om ) /\ A e. B ) -> A e. _om )
4 nnord
 |-  ( B e. _om -> Ord B )
5 ordsucss
 |-  ( Ord B -> ( A e. B -> suc A C_ B ) )
6 4 5 syl
 |-  ( B e. _om -> ( A e. B -> suc A C_ B ) )
7 6 ad2antlr
 |-  ( ( ( C e. _om /\ B e. _om ) /\ A e. _om ) -> ( A e. B -> suc A C_ B ) )
8 peano2b
 |-  ( A e. _om <-> suc A e. _om )
9 oveq2
 |-  ( x = suc A -> ( C +o x ) = ( C +o suc A ) )
10 9 sseq2d
 |-  ( x = suc A -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o suc A ) ) )
11 10 imbi2d
 |-  ( x = suc A -> ( ( C e. _om -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. _om -> ( C +o suc A ) C_ ( C +o suc A ) ) ) )
12 oveq2
 |-  ( x = y -> ( C +o x ) = ( C +o y ) )
13 12 sseq2d
 |-  ( x = y -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o y ) ) )
14 13 imbi2d
 |-  ( x = y -> ( ( C e. _om -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. _om -> ( C +o suc A ) C_ ( C +o y ) ) ) )
15 oveq2
 |-  ( x = suc y -> ( C +o x ) = ( C +o suc y ) )
16 15 sseq2d
 |-  ( x = suc y -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o suc y ) ) )
17 16 imbi2d
 |-  ( x = suc y -> ( ( C e. _om -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. _om -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
18 oveq2
 |-  ( x = B -> ( C +o x ) = ( C +o B ) )
19 18 sseq2d
 |-  ( x = B -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o B ) ) )
20 19 imbi2d
 |-  ( x = B -> ( ( C e. _om -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. _om -> ( C +o suc A ) C_ ( C +o B ) ) ) )
21 ssid
 |-  ( C +o suc A ) C_ ( C +o suc A )
22 21 2a1i
 |-  ( suc A e. _om -> ( C e. _om -> ( C +o suc A ) C_ ( C +o suc A ) ) )
23 sssucid
 |-  ( C +o y ) C_ suc ( C +o y )
24 sstr2
 |-  ( ( C +o suc A ) C_ ( C +o y ) -> ( ( C +o y ) C_ suc ( C +o y ) -> ( C +o suc A ) C_ suc ( C +o y ) ) )
25 23 24 mpi
 |-  ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ suc ( C +o y ) )
26 nnasuc
 |-  ( ( C e. _om /\ y e. _om ) -> ( C +o suc y ) = suc ( C +o y ) )
27 26 ancoms
 |-  ( ( y e. _om /\ C e. _om ) -> ( C +o suc y ) = suc ( C +o y ) )
28 27 sseq2d
 |-  ( ( y e. _om /\ C e. _om ) -> ( ( C +o suc A ) C_ ( C +o suc y ) <-> ( C +o suc A ) C_ suc ( C +o y ) ) )
29 25 28 syl5ibr
 |-  ( ( y e. _om /\ C e. _om ) -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) )
30 29 ex
 |-  ( y e. _om -> ( C e. _om -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
31 30 ad2antrr
 |-  ( ( ( y e. _om /\ suc A e. _om ) /\ suc A C_ y ) -> ( C e. _om -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
32 31 a2d
 |-  ( ( ( y e. _om /\ suc A e. _om ) /\ suc A C_ y ) -> ( ( C e. _om -> ( C +o suc A ) C_ ( C +o y ) ) -> ( C e. _om -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
33 11 14 17 20 22 32 findsg
 |-  ( ( ( B e. _om /\ suc A e. _om ) /\ suc A C_ B ) -> ( C e. _om -> ( C +o suc A ) C_ ( C +o B ) ) )
34 33 exp31
 |-  ( B e. _om -> ( suc A e. _om -> ( suc A C_ B -> ( C e. _om -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
35 8 34 syl5bi
 |-  ( B e. _om -> ( A e. _om -> ( suc A C_ B -> ( C e. _om -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
36 35 com4r
 |-  ( C e. _om -> ( B e. _om -> ( A e. _om -> ( suc A C_ B -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
37 36 imp31
 |-  ( ( ( C e. _om /\ B e. _om ) /\ A e. _om ) -> ( suc A C_ B -> ( C +o suc A ) C_ ( C +o B ) ) )
38 nnasuc
 |-  ( ( C e. _om /\ A e. _om ) -> ( C +o suc A ) = suc ( C +o A ) )
39 38 sseq1d
 |-  ( ( C e. _om /\ A e. _om ) -> ( ( C +o suc A ) C_ ( C +o B ) <-> suc ( C +o A ) C_ ( C +o B ) ) )
40 ovex
 |-  ( C +o A ) e. _V
41 sucssel
 |-  ( ( C +o A ) e. _V -> ( suc ( C +o A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
42 40 41 ax-mp
 |-  ( suc ( C +o A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) )
43 39 42 syl6bi
 |-  ( ( C e. _om /\ A e. _om ) -> ( ( C +o suc A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
44 43 adantlr
 |-  ( ( ( C e. _om /\ B e. _om ) /\ A e. _om ) -> ( ( C +o suc A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
45 7 37 44 3syld
 |-  ( ( ( C e. _om /\ B e. _om ) /\ A e. _om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
46 45 imp
 |-  ( ( ( ( C e. _om /\ B e. _om ) /\ A e. _om ) /\ A e. B ) -> ( C +o A ) e. ( C +o B ) )
47 46 an32s
 |-  ( ( ( ( C e. _om /\ B e. _om ) /\ A e. B ) /\ A e. _om ) -> ( C +o A ) e. ( C +o B ) )
48 3 47 mpdan
 |-  ( ( ( C e. _om /\ B e. _om ) /\ A e. B ) -> ( C +o A ) e. ( C +o B ) )
49 48 ex
 |-  ( ( C e. _om /\ B e. _om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
50 49 ancoms
 |-  ( ( B e. _om /\ C e. _om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )