Metamath Proof Explorer

Theorem nnaword1

Description: Weak ordering property of addition. (Contributed by NM, 9-Nov-2002) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 nna0 
 |-  ( A e. _om -> ( A +o (/) ) = A )
2 1 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o (/) ) = A )
3 0ss 
 |-  (/) C_ B
4 peano1 
 |-  (/) e. _om
5 nnaword 
 |-  ( ( (/) e. _om /\ B e. _om /\ A e. _om ) -> ( (/) C_ B <-> ( A +o (/) ) C_ ( A +o B ) ) )
6 5 3com13 
 |-  ( ( A e. _om /\ B e. _om /\ (/) e. _om ) -> ( (/) C_ B <-> ( A +o (/) ) C_ ( A +o B ) ) )
7 4 6 mp3an3 
 |-  ( ( A e. _om /\ B e. _om ) -> ( (/) C_ B <-> ( A +o (/) ) C_ ( A +o B ) ) )
8 3 7 mpbii 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o (/) ) C_ ( A +o B ) )
9 2 8 eqsstrrd 
 |-  ( ( A e. _om /\ B e. _om ) -> A C_ ( A +o B ) )