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

Metamath Proof Explorer

Theorem oaword2

Description: An ordinal is less than or equal to its sum with another. Theorem 21 of Suppes p. 209. Lemma 3.3 of Schloeder p. 7. (Contributed by NM, 7-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ B
2 0elon 
 |-  (/) e. On
3 oawordri 
 |-  ( ( (/) e. On /\ B e. On /\ A e. On ) -> ( (/) C_ B -> ( (/) +o A ) C_ ( B +o A ) ) )
4 2 3 mp3an1 
 |-  ( ( B e. On /\ A e. On ) -> ( (/) C_ B -> ( (/) +o A ) C_ ( B +o A ) ) )
5 oa0r 
 |-  ( A e. On -> ( (/) +o A ) = A )
6 5 adantl 
 |-  ( ( B e. On /\ A e. On ) -> ( (/) +o A ) = A )
7 6 sseq1d 
 |-  ( ( B e. On /\ A e. On ) -> ( ( (/) +o A ) C_ ( B +o A ) <-> A C_ ( B +o A ) ) )
8 4 7 sylibd 
 |-  ( ( B e. On /\ A e. On ) -> ( (/) C_ B -> A C_ ( B +o A ) ) )
9 1 8 mpi 
 |-  ( ( B e. On /\ A e. On ) -> A C_ ( B +o A ) )
10 9 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> A C_ ( B +o A ) )