Theorem nnacl 6420

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.)

Assertion

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

Proof of Theorem nnacl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 5826	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 +o 𝑥) = (𝐴 +o 𝐵))
2	1	eleq1d 2226	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 +o 𝑥) ∈ ω ↔ (𝐴 +o 𝐵) ∈ ω))
3	2	imbi2d 229	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ ω → (𝐴 +o 𝑥) ∈ ω) ↔ (𝐴 ∈ ω → (𝐴 +o 𝐵) ∈ ω)))
4		oveq2 5826	. . . . 5 ⊢ (𝑥 = ∅ → (𝐴 +o 𝑥) = (𝐴 +o ∅))
5	4	eleq1d 2226	. . . 4 ⊢ (𝑥 = ∅ → ((𝐴 +o 𝑥) ∈ ω ↔ (𝐴 +o ∅) ∈ ω))
6		oveq2 5826	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐴 +o 𝑥) = (𝐴 +o 𝑦))
7	6	eleq1d 2226	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐴 +o 𝑥) ∈ ω ↔ (𝐴 +o 𝑦) ∈ ω))
8		oveq2 5826	. . . . 5 ⊢ (𝑥 = suc 𝑦 → (𝐴 +o 𝑥) = (𝐴 +o suc 𝑦))
9	8	eleq1d 2226	. . . 4 ⊢ (𝑥 = suc 𝑦 → ((𝐴 +o 𝑥) ∈ ω ↔ (𝐴 +o suc 𝑦) ∈ ω))
10		nna0 6414	. . . . . 6 ⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴)
11	10	eleq1d 2226	. . . . 5 ⊢ (𝐴 ∈ ω → ((𝐴 +o ∅) ∈ ω ↔ 𝐴 ∈ ω))
12	11	ibir 176	. . . 4 ⊢ (𝐴 ∈ ω → (𝐴 +o ∅) ∈ ω)
13		peano2 4552	. . . . . 6 ⊢ ((𝐴 +o 𝑦) ∈ ω → suc (𝐴 +o 𝑦) ∈ ω)
14		nnasuc 6416	. . . . . . 7 ⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o suc 𝑦) = suc (𝐴 +o 𝑦))
15	14	eleq1d 2226	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 +o suc 𝑦) ∈ ω ↔ suc (𝐴 +o 𝑦) ∈ ω))
16	13, 15	syl5ibr 155	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 +o 𝑦) ∈ ω → (𝐴 +o suc 𝑦) ∈ ω))
17	16	expcom 115	. . . 4 ⊢ (𝑦 ∈ ω → (𝐴 ∈ ω → ((𝐴 +o 𝑦) ∈ ω → (𝐴 +o suc 𝑦) ∈ ω)))
18	5, 7, 9, 12, 17	finds2 4558	. . 3 ⊢ (𝑥 ∈ ω → (𝐴 ∈ ω → (𝐴 +o 𝑥) ∈ ω))
19	3, 18	vtoclga 2778	. 2 ⊢ (𝐵 ∈ ω → (𝐴 ∈ ω → (𝐴 +o 𝐵) ∈ ω))
20	19	impcom 124	1 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) ∈ ω)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1335   ∈ wcel 2128  ∅c0 3394  suc csuc 4324  ωcom 4547  (class class class)co 5818   +_o coa 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4252  df-iord 4325  df-on 4327  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-f1 5172  df-fo 5173  df-f1o 5174  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1st 6082  df-2nd 6083  df-recs 6246  df-irdg 6311  df-oadd 6361

This theorem is referenced by:  nnmcl  6421  nnacli  6422  nnaass  6425  nndi  6426  nndir  6430  nnaordi  6448  nnaord  6449  nnaword  6451  addclpi  7230  nnppipi  7246  archnqq  7320  addcmpblnq0  7346  addclnq0  7354  nnanq0  7361  distrnq0  7362  addassnq0lemcl  7364  prarloclemlt  7396  prarloclemlo  7397  prarloclem3  7400  omgadd  10658  hashunlem  10660  hashun  10661