Theorem peano2nn 5883

Description: Peano postulate: a successor of a natural number is a natural number.

Assertion

Ref	Expression
peano2nn	⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)

Proof of Theorem peano2nn

Step	Hyp	Ref	Expression
1		opreq1 3953	. . 3 ⊢ (z = A → (z + 1) = (A + 1))
2	1	eleq1d 1532	. 2 ⊢ (z = A → ((z + 1) ∈ ℕ ↔ (A + 1) ∈ ℕ))
3		opreq1 3953	. . . . . . . . 9 ⊢ (y = z → (y + 1) = (z + 1))
4	3	eleq1d 1532	. . . . . . . 8 ⊢ (y = z → ((y + 1) ∈ x ↔ (z + 1) ∈ x))
5	4	rcla4cv 1865	. . . . . . 7 ⊢ (∀y ∈ x (y + 1) ∈ x → (z ∈ x → (z + 1) ∈ x))
6	5	adantl 388	. . . . . 6 ⊢ ((1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x) → (z ∈ x → (z + 1) ∈ x))
7	6	a2i 9	. . . . 5 ⊢ (((1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x) → z ∈ x) → ((1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x) → (z + 1) ∈ x))
8	7	19.20i 989	. . . 4 ⊢ (∀x((1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x) → z ∈ x) → ∀x((1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x) → (z + 1) ∈ x))
9		visset 1804	. . . . 5 ⊢ z ∈ V
10	9	elintab 2534	. . . 4 ⊢ (z ∈ ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)} ↔ ∀x((1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x) → z ∈ x))
11		oprex 3968	. . . . 5 ⊢ (z + 1) ∈ V
12	11	elintab 2534	. . . 4 ⊢ ((z + 1) ∈ ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)} ↔ ∀x((1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x) → (z + 1) ∈ x))
13	8, 10, 12	3imtr4 219	. . 3 ⊢ (z ∈ ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)} → (z + 1) ∈ ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)})
14		df-n 5873	. . . 4 ⊢ ℕ = ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)}
15	14	eleq2i 1530	. . 3 ⊢ (z ∈ ℕ ↔ z ∈ ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)})
16	14	eleq2i 1530	. . 3 ⊢ ((z + 1) ∈ ℕ ↔ (z + 1) ∈ ∩{x∣(1 ∈ x ⋀ ∀y ∈ x (y + 1) ∈ x)})
17	13, 15, 16	3imtr4 219	. 2 ⊢ (z ∈ ℕ → (z + 1) ∈ ℕ)
18	2, 17	vtoclga 1843	1 ⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  {cab 1456  ∀wral 1637  ∩cint 2523  (class class class)co 3948  1c1 5207   + caddc 5209  ℕcn 5268

This theorem is referenced by:  dfnn2 5884  nnind 5885  nnaddclt 5888  nnleltp1t 5901  nnltp1let 5902  nnsub 5903  nnunb 6017  elnn0nn 6118  nneo 6144  monoord 6231  seq1lem2 6247  seq1suclem 6253  seq1res 6264  ser1recl 6268  ser1p1 6273  ser1mono 6274  ser1add2 6275  ser1add 6276  expp1t 6506  seq1bnd 6847  ser1absdiflem 6866  facp1t 6873  bccl2t 6909  binomlem5 7008  caucvglem5 7097  ser1const 7107  ser1cmp 7110  ser1cmp2 7113  cvgcmp2lem 7116  fnsmnt 7161  cvgratlem1ALT 7182  cvgratlem3ALT 7184  cvgratlem1 7185  cvgratlem3 7187  cvgratlem4 7188  efcltlem1 7246  ef1tllem 7323  eirrlem1 7330  eirrlem3 7332  eirrlem5 7334  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  acdcALT 7438  infpnlem1 7449  infpnlem2 7450  ruclem8 7460  ruclem15 7467  ruclem18 7470  ruclem19 7471  ruclem20 7472  ruclem21 7473  ruclem24 7476  ruclem26 7478  ruclem27 7479  ruclem28 7480  ruclem30 7482  ruclem31 7483  ruclem35 7487  fsumcnlem 7923  bcthlem2 7934  bcthlem17 7949  bcthlem18 7950

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-int 2524  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188  df-opr 3950  df-n 5873

Copyright terms: Public domain