Metamath Proof Explorer


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 On B On A B + 𝑜 A

Proof

Step Hyp Ref Expression
1 0ss B
2 0elon On
3 oawordri On B On A On B + 𝑜 A B + 𝑜 A
4 2 3 mp3an1 B On A On B + 𝑜 A B + 𝑜 A
5 oa0r A On + 𝑜 A = A
6 5 adantl B On A On + 𝑜 A = A
7 6 sseq1d B On A On + 𝑜 A B + 𝑜 A A B + 𝑜 A
8 4 7 sylibd B On A On B A B + 𝑜 A
9 1 8 mpi B On A On A B + 𝑜 A
10 9 ancoms A On B On A B + 𝑜 A