This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) ∈ ω )