Theorem oaword2

Description: An ordinal is less than or equal to its sum with another. Theorem 21 of Suppes p. 209. (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 ) )