Theorem peano2 4699

Description: The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
peano2	⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Proof of Theorem peano2

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

Step	Hyp	Ref	Expression
1		elex 2815	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ V)
2		simpl 109	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → 𝐴 ∈ V)
3		eleq1 2294	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝐴 ∈ 𝑧))
4		suceq 4505	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → suc 𝑥 = suc 𝐴)
5	4	eleq1d 2300	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (suc 𝑥 ∈ 𝑧 ↔ suc 𝐴 ∈ 𝑧))
6	3, 5	imbi12d 234	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧) ↔ (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧)))
7	6	adantl 277	. . . . . 6 ⊢ (((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) ∧ 𝑥 = 𝐴) → ((𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧) ↔ (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧)))
8		df-clab 2218	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
9		simpr 110	. . . . . . . . . . . 12 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
10		df-ral 2516	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦 ↔ ∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
11	9, 10	sylib 122	. . . . . . . . . . 11 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
12	11	sbimi 1812	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
13		sbim 2006	. . . . . . . . . . . 12 ⊢ ([𝑧 / 𝑦](𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ ([𝑧 / 𝑦]𝑥 ∈ 𝑦 → [𝑧 / 𝑦]suc 𝑥 ∈ 𝑦))
14		clelsb2 2337	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑦]𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧)
15		clelsb2 2337	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑦]suc 𝑥 ∈ 𝑦 ↔ suc 𝑥 ∈ 𝑧)
16	14, 15	imbi12i 239	. . . . . . . . . . . 12 ⊢ (([𝑧 / 𝑦]𝑥 ∈ 𝑦 → [𝑧 / 𝑦]suc 𝑥 ∈ 𝑦) ↔ (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
17	13, 16	bitri 184	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑦](𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
18	17	sbalv 2058	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑦]∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
19	12, 18	sylib 122	. . . . . . . . 9 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
20	8, 19	sylbi 121	. . . . . . . 8 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
21	20	19.21bi 1607	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
22	21	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
23		nfv 1577	. . . . . . 7 ⊢ Ⅎ𝑥 𝐴 ∈ V
24		nfv 1577	. . . . . . . . 9 ⊢ Ⅎ𝑥∅ ∈ 𝑦
25		nfra1 2564	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦
26	24, 25	nfan 1614	. . . . . . . 8 ⊢ Ⅎ𝑥(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
27	26	nfsab 2223	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
28	23, 27	nfan 1614	. . . . . 6 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})
29		nfcvd 2376	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → Ⅎ𝑥𝐴)
30		nfvd 1578	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → Ⅎ𝑥(𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
31	2, 7, 22, 28, 29, 30	vtocldf 2856	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
32	31	ralrimiva 2606	. . . 4 ⊢ (𝐴 ∈ V → ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
33		ralim 2592	. . . . 5 ⊢ (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧) → (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}𝐴 ∈ 𝑧 → ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧))
34		elintg 3941	. . . . . 6 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}𝐴 ∈ 𝑧))
35		sucexg 4602	. . . . . . 7 ⊢ (𝐴 ∈ V → suc 𝐴 ∈ V)
36		elintg 3941	. . . . . . 7 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧))
37	35, 36	syl 14	. . . . . 6 ⊢ (𝐴 ∈ V → (suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧))
38	34, 37	imbi12d 234	. . . . 5 ⊢ (𝐴 ∈ V → ((𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) ↔ (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}𝐴 ∈ 𝑧 → ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧)))
39	33, 38	imbitrrid 156	. . . 4 ⊢ (𝐴 ∈ V → (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧) → (𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})))
40	32, 39	mpd 13	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}))
41		dfom3 4696	. . . 4 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
42	41	eleq2i 2298	. . 3 ⊢ (𝐴 ∈ ω ↔ 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})
43	41	eleq2i 2298	. . 3 ⊢ (suc 𝐴 ∈ ω ↔ suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})
44	40, 42, 43	3imtr4g 205	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ω → suc 𝐴 ∈ ω))
45	1, 44	mpcom 36	1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1396   = wceq 1398  [wsb 1810   ∈ wcel 2202  {cab 2217  ∀wral 2511  Vcvv 2803  ∅c0 3496  ∩ cint 3933  suc csuc 4468  ωcom 4694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-uni 3899  df-int 3934  df-suc 4474  df-iom 4695

This theorem is referenced by:  peano5  4702  limom  4718  peano2b  4719  nnregexmid  4725  omsinds  4726  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecrdg  6617  nnacl  6691  nnacom  6695  nnmsucr  6699  nnsucsssuc  6703  nnaword  6722  1onn  6731  2onn  6732  3onn  6733  4onn  6734  nnaordex  6739  php5  7087  phplem4dom  7091  php5dom  7092  phplem4on  7097  dif1en  7111  findcard  7120  findcard2  7121  findcard2s  7122  infnfi  7127  unsnfi  7154  omp1eomlem  7336  ctmlemr  7350  nninfninc  7365  infnninf  7366  infnninfOLD  7367  nnnninf  7368  nnnninfeq  7370  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  frec2uzrand  10713  frecuzrdgsuc  10722  frecuzrdgsuctlem  10731  frecfzennn  10734  hashunlem  11113  ennnfonelemk  13084  ennnfonelemg  13087  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemrn  13103  ennnfonelemnn0  13106  ctinfomlemom  13111  0nninf  16713  nnsf  16714  peano4nninf  16715  nninfsellemdc  16719  nninfsellemsuc  16721  nninfself  16722  nninfsellemeqinf  16725  nnnninfex  16731