Theorem oaword2

Description: An ordinal is less than or equal to its sum with another. Theorem 21 of Suppes p. 209. Lemma 3.3 of Schloeder p. 7. (Contributed by NM, 7-Dec-2004)

	Ref	Expression
Assertion	oaword2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐵 +o 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝐵
2		0elon	⊢ ∅ ∈ On
3		oawordri	⊢ ( ( ∅ ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ⊆ 𝐵 → ( ∅ +o 𝐴 ) ⊆ ( 𝐵 +o 𝐴 ) ) )
4	2 3	mp3an1	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ⊆ 𝐵 → ( ∅ +o 𝐴 ) ⊆ ( 𝐵 +o 𝐴 ) ) )
5		oa0r	⊢ ( 𝐴 ∈ On → ( ∅ +o 𝐴 ) = 𝐴 )
6	5	adantl	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ +o 𝐴 ) = 𝐴 )
7	6	sseq1d	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ( ∅ +o 𝐴 ) ⊆ ( 𝐵 +o 𝐴 ) ↔ 𝐴 ⊆ ( 𝐵 +o 𝐴 ) ) )
8	4 7	sylibd	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ⊆ 𝐵 → 𝐴 ⊆ ( 𝐵 +o 𝐴 ) ) )
9	1 8	mpi	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → 𝐴 ⊆ ( 𝐵 +o 𝐴 ) )
10	9	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐵 +o 𝐴 ) )