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