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

Metamath Proof Explorer

Theorem oaword1

Description: An ordinal is less than or equal to its sum with another. Part of Exercise 5 of TakeutiZaring p. 62. Lemma 3.2 of Schloeder p. 7. (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 ) )