Theorem oaword1

Description: An ordinal is less than or equal to its sum with another. Part of Exercise 5 of TakeutiZaring p. 62. (For the other part see oaord1 .) (Contributed by NM, 6-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		oa0	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o ∅ ) = 𝐴 )
3		0ss	⊢ ∅ ⊆ 𝐵
4		0elon	⊢ ∅ ∈ On
5		oaword	⊢ ( ( ∅ ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ⊆ 𝐵 ↔ ( 𝐴 +o ∅ ) ⊆ ( 𝐴 +o 𝐵 ) ) )
6	5	3com13	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ∅ ∈ On ) → ( ∅ ⊆ 𝐵 ↔ ( 𝐴 +o ∅ ) ⊆ ( 𝐴 +o 𝐵 ) ) )
7	4 6	mp3an3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ⊆ 𝐵 ↔ ( 𝐴 +o ∅ ) ⊆ ( 𝐴 +o 𝐵 ) ) )
8	3 7	mpbii	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o ∅ ) ⊆ ( 𝐴 +o 𝐵 ) )
9	2 8	eqsstrrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐴 +o 𝐵 ) )