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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐵 ↔ 𝐴 ∈ ( 𝐴 +o 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2		oaord	⊢ ( ( ∅ ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐵 ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝐵 ) ) )
3	1 2	mp3an1	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐵 ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝐵 ) ) )
4		oa0	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
5	4	adantl	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐴 +o ∅ ) = 𝐴 )
6	5	eleq1d	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝐵 ) ↔ 𝐴 ∈ ( 𝐴 +o 𝐵 ) ) )
7	3 6	bitrd	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐵 ↔ 𝐴 ∈ ( 𝐴 +o 𝐵 ) ) )
8	7	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐵 ↔ 𝐴 ∈ ( 𝐴 +o 𝐵 ) ) )