Theorem nnacl

Description: Closure of addition of natural numbers. Proposition 8.9 of TakeutiZaring p. 59. Theorem 2.20 of Schloeder p. 6. (Contributed by NM, 20-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Assertion	nnacl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝐵 ) )
2	1	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 +o 𝑥 ) ∈ ω ↔ ( 𝐴 +o 𝐵 ) ∈ ω ) )
3	2	imbi2d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ ω → ( 𝐴 +o 𝑥 ) ∈ ω ) ↔ ( 𝐴 ∈ ω → ( 𝐴 +o 𝐵 ) ∈ ω ) ) )
4		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∅ ) )
5	4	eleq1d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 +o 𝑥 ) ∈ ω ↔ ( 𝐴 +o ∅ ) ∈ ω ) )
6		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
7	6	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 +o 𝑥 ) ∈ ω ↔ ( 𝐴 +o 𝑦 ) ∈ ω ) )
8		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o suc 𝑦 ) )
9	8	eleq1d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 +o 𝑥 ) ∈ ω ↔ ( 𝐴 +o suc 𝑦 ) ∈ ω ) )
10		nna0	⊢ ( 𝐴 ∈ ω → ( 𝐴 +o ∅ ) = 𝐴 )
11	10	eleq1d	⊢ ( 𝐴 ∈ ω → ( ( 𝐴 +o ∅ ) ∈ ω ↔ 𝐴 ∈ ω ) )
12	11	ibir	⊢ ( 𝐴 ∈ ω → ( 𝐴 +o ∅ ) ∈ ω )
13		peano2	⊢ ( ( 𝐴 +o 𝑦 ) ∈ ω → suc ( 𝐴 +o 𝑦 ) ∈ ω )
14		nnasuc	⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
15	14	eleq1d	⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o suc 𝑦 ) ∈ ω ↔ suc ( 𝐴 +o 𝑦 ) ∈ ω ) )
16	13 15	imbitrrid	⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o 𝑦 ) ∈ ω → ( 𝐴 +o suc 𝑦 ) ∈ ω ) )
17	16	expcom	⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐴 +o 𝑦 ) ∈ ω → ( 𝐴 +o suc 𝑦 ) ∈ ω ) ) )
18	5 7 9 12 17	finds2	⊢ ( 𝑥 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 +o 𝑥 ) ∈ ω ) )
19	3 18	vtoclga	⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 +o 𝐵 ) ∈ ω ) )
20	19	impcom	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ∈ ω )