Metamath Proof Explorer


Theorem nnawordi

Description: Adding to both sides of an inequality in _om . (Contributed by Scott Fenton, 16-Apr-2012) (Revised by Mario Carneiro, 12-May-2012)

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

Proof

Step Hyp Ref Expression
1 oveq2
 |-  ( x = (/) -> ( A +o x ) = ( A +o (/) ) )
2 oveq2
 |-  ( x = (/) -> ( B +o x ) = ( B +o (/) ) )
3 1 2 sseq12d
 |-  ( x = (/) -> ( ( A +o x ) C_ ( B +o x ) <-> ( A +o (/) ) C_ ( B +o (/) ) ) )
4 3 imbi2d
 |-  ( x = (/) -> ( ( A C_ B -> ( A +o x ) C_ ( B +o x ) ) <-> ( A C_ B -> ( A +o (/) ) C_ ( B +o (/) ) ) ) )
5 4 imbi2d
 |-  ( x = (/) -> ( ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o x ) C_ ( B +o x ) ) ) <-> ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o (/) ) C_ ( B +o (/) ) ) ) ) )
6 oveq2
 |-  ( x = y -> ( A +o x ) = ( A +o y ) )
7 oveq2
 |-  ( x = y -> ( B +o x ) = ( B +o y ) )
8 6 7 sseq12d
 |-  ( x = y -> ( ( A +o x ) C_ ( B +o x ) <-> ( A +o y ) C_ ( B +o y ) ) )
9 8 imbi2d
 |-  ( x = y -> ( ( A C_ B -> ( A +o x ) C_ ( B +o x ) ) <-> ( A C_ B -> ( A +o y ) C_ ( B +o y ) ) ) )
10 9 imbi2d
 |-  ( x = y -> ( ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o x ) C_ ( B +o x ) ) ) <-> ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o y ) C_ ( B +o y ) ) ) ) )
11 oveq2
 |-  ( x = suc y -> ( A +o x ) = ( A +o suc y ) )
12 oveq2
 |-  ( x = suc y -> ( B +o x ) = ( B +o suc y ) )
13 11 12 sseq12d
 |-  ( x = suc y -> ( ( A +o x ) C_ ( B +o x ) <-> ( A +o suc y ) C_ ( B +o suc y ) ) )
14 13 imbi2d
 |-  ( x = suc y -> ( ( A C_ B -> ( A +o x ) C_ ( B +o x ) ) <-> ( A C_ B -> ( A +o suc y ) C_ ( B +o suc y ) ) ) )
15 14 imbi2d
 |-  ( x = suc y -> ( ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o x ) C_ ( B +o x ) ) ) <-> ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o suc y ) C_ ( B +o suc y ) ) ) ) )
16 oveq2
 |-  ( x = C -> ( A +o x ) = ( A +o C ) )
17 oveq2
 |-  ( x = C -> ( B +o x ) = ( B +o C ) )
18 16 17 sseq12d
 |-  ( x = C -> ( ( A +o x ) C_ ( B +o x ) <-> ( A +o C ) C_ ( B +o C ) ) )
19 18 imbi2d
 |-  ( x = C -> ( ( A C_ B -> ( A +o x ) C_ ( B +o x ) ) <-> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) )
20 19 imbi2d
 |-  ( x = C -> ( ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o x ) C_ ( B +o x ) ) ) <-> ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) ) )
21 nnon
 |-  ( A e. _om -> A e. On )
22 nnon
 |-  ( B e. _om -> B e. On )
23 oa0
 |-  ( A e. On -> ( A +o (/) ) = A )
24 23 adantr
 |-  ( ( A e. On /\ B e. On ) -> ( A +o (/) ) = A )
25 oa0
 |-  ( B e. On -> ( B +o (/) ) = B )
26 25 adantl
 |-  ( ( A e. On /\ B e. On ) -> ( B +o (/) ) = B )
27 24 26 sseq12d
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o (/) ) C_ ( B +o (/) ) <-> A C_ B ) )
28 27 biimprd
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +o (/) ) C_ ( B +o (/) ) ) )
29 21 22 28 syl2an
 |-  ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o (/) ) C_ ( B +o (/) ) ) )
30 nnacl
 |-  ( ( A e. _om /\ y e. _om ) -> ( A +o y ) e. _om )
31 30 ancoms
 |-  ( ( y e. _om /\ A e. _om ) -> ( A +o y ) e. _om )
32 31 adantrr
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> ( A +o y ) e. _om )
33 nnon
 |-  ( ( A +o y ) e. _om -> ( A +o y ) e. On )
34 eloni
 |-  ( ( A +o y ) e. On -> Ord ( A +o y ) )
35 32 33 34 3syl
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> Ord ( A +o y ) )
36 nnacl
 |-  ( ( B e. _om /\ y e. _om ) -> ( B +o y ) e. _om )
37 36 ancoms
 |-  ( ( y e. _om /\ B e. _om ) -> ( B +o y ) e. _om )
38 37 adantrl
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> ( B +o y ) e. _om )
39 nnon
 |-  ( ( B +o y ) e. _om -> ( B +o y ) e. On )
40 eloni
 |-  ( ( B +o y ) e. On -> Ord ( B +o y ) )
41 38 39 40 3syl
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> Ord ( B +o y ) )
42 ordsucsssuc
 |-  ( ( Ord ( A +o y ) /\ Ord ( B +o y ) ) -> ( ( A +o y ) C_ ( B +o y ) <-> suc ( A +o y ) C_ suc ( B +o y ) ) )
43 35 41 42 syl2anc
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> ( ( A +o y ) C_ ( B +o y ) <-> suc ( A +o y ) C_ suc ( B +o y ) ) )
44 43 biimpa
 |-  ( ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) /\ ( A +o y ) C_ ( B +o y ) ) -> suc ( A +o y ) C_ suc ( B +o y ) )
45 nnasuc
 |-  ( ( A e. _om /\ y e. _om ) -> ( A +o suc y ) = suc ( A +o y ) )
46 45 ancoms
 |-  ( ( y e. _om /\ A e. _om ) -> ( A +o suc y ) = suc ( A +o y ) )
47 46 adantrr
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> ( A +o suc y ) = suc ( A +o y ) )
48 nnasuc
 |-  ( ( B e. _om /\ y e. _om ) -> ( B +o suc y ) = suc ( B +o y ) )
49 48 ancoms
 |-  ( ( y e. _om /\ B e. _om ) -> ( B +o suc y ) = suc ( B +o y ) )
50 49 adantrl
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> ( B +o suc y ) = suc ( B +o y ) )
51 47 50 sseq12d
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> ( ( A +o suc y ) C_ ( B +o suc y ) <-> suc ( A +o y ) C_ suc ( B +o y ) ) )
52 51 adantr
 |-  ( ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) /\ ( A +o y ) C_ ( B +o y ) ) -> ( ( A +o suc y ) C_ ( B +o suc y ) <-> suc ( A +o y ) C_ suc ( B +o y ) ) )
53 44 52 mpbird
 |-  ( ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) /\ ( A +o y ) C_ ( B +o y ) ) -> ( A +o suc y ) C_ ( B +o suc y ) )
54 53 ex
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> ( ( A +o y ) C_ ( B +o y ) -> ( A +o suc y ) C_ ( B +o suc y ) ) )
55 54 imim2d
 |-  ( ( y e. _om /\ ( A e. _om /\ B e. _om ) ) -> ( ( A C_ B -> ( A +o y ) C_ ( B +o y ) ) -> ( A C_ B -> ( A +o suc y ) C_ ( B +o suc y ) ) ) )
56 55 ex
 |-  ( y e. _om -> ( ( A e. _om /\ B e. _om ) -> ( ( A C_ B -> ( A +o y ) C_ ( B +o y ) ) -> ( A C_ B -> ( A +o suc y ) C_ ( B +o suc y ) ) ) ) )
57 56 a2d
 |-  ( y e. _om -> ( ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o y ) C_ ( B +o y ) ) ) -> ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o suc y ) C_ ( B +o suc y ) ) ) ) )
58 5 10 15 20 29 57 finds
 |-  ( C e. _om -> ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) )
59 58 com12
 |-  ( ( A e. _om /\ B e. _om ) -> ( C e. _om -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) )
60 59 3impia
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )