Theorem oaword1

Description: An ordinal is less than or equal to its sum with another. Part of Exercise 5 of TakeutiZaring p. 62. (For the other part see oaord1 .) (Contributed by NM, 6-Dec-2004)

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

Proof

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