Metamath Proof Explorer

Theorem nnacl

Description: Closure of addition of natural numbers. Proposition 8.9 of TakeutiZaring p. 59. (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 syl5ibr ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +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 𝐵 ) ∈ ω )