This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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