Metamath Proof Explorer

Theorem oaord1

Description: An ordinal is less than its sum with a nonzero ordinal. Theorem 18 of Suppes p. 209 and its converse. (Contributed by NM, 6-Dec-2004)

Ref Expression
Assertion oaord1 ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ B ↔ A ∈ A + 𝑜 B

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 oaord ⊢ ∅ ∈ On ∧ B ∈ On ∧ A ∈ On → ∅ ∈ B ↔ A + 𝑜 ∅ ∈ A + 𝑜 B
3 1 2 mp3an1 ⊢ B ∈ On ∧ A ∈ On → ∅ ∈ B ↔ A + 𝑜 ∅ ∈ A + 𝑜 B
4 oa0 ⊢ A ∈ On → A + 𝑜 ∅ = A
5 4 adantl ⊢ B ∈ On ∧ A ∈ On → A + 𝑜 ∅ = A
6 5 eleq1d ⊢ B ∈ On ∧ A ∈ On → A + 𝑜 ∅ ∈ A + 𝑜 B ↔ A ∈ A + 𝑜 B
7 3 6 bitrd ⊢ B ∈ On ∧ A ∈ On → ∅ ∈ B ↔ A ∈ A + 𝑜 B
8 7 ancoms ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ B ↔ A ∈ A + 𝑜 B