Theorem peano2 4517

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 2700	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ V)
2		simpl 108	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → 𝐴 ∈ V)
3		eleq1 2203	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝐴 ∈ 𝑧))
4		suceq 4332	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → suc 𝑥 = suc 𝐴)
5	4	eleq1d 2209	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (suc 𝑥 ∈ 𝑧 ↔ suc 𝐴 ∈ 𝑧))
6	3, 5	imbi12d 233	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧) ↔ (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧)))
7	6	adantl 275	. . . . . 6 ⊢ (((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) ∧ 𝑥 = 𝐴) → ((𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧) ↔ (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧)))
8		df-clab 2127	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
9		simpr 109	. . . . . . . . . . . 12 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
10		df-ral 2422	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦 ↔ ∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
11	9, 10	sylib 121	. . . . . . . . . . 11 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
12	11	sbimi 1738	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
13		sbim 1927	. . . . . . . . . . . 12 ⊢ ([𝑧 / 𝑦](𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ ([𝑧 / 𝑦]𝑥 ∈ 𝑦 → [𝑧 / 𝑦]suc 𝑥 ∈ 𝑦))
14		clelsb4 2246	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑦]𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧)
15		clelsb4 2246	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑦]suc 𝑥 ∈ 𝑦 ↔ suc 𝑥 ∈ 𝑧)
16	14, 15	imbi12i 238	. . . . . . . . . . . 12 ⊢ (([𝑧 / 𝑦]𝑥 ∈ 𝑦 → [𝑧 / 𝑦]suc 𝑥 ∈ 𝑦) ↔ (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
17	13, 16	bitri 183	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑦](𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
18	17	sbalv 1981	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑦]∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
19	12, 18	sylib 121	. . . . . . . . 9 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
20	8, 19	sylbi 120	. . . . . . . 8 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
21	20	19.21bi 1538	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
22	21	adantl 275	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
23		nfv 1509	. . . . . . 7 ⊢ Ⅎ𝑥 𝐴 ∈ V
24		nfv 1509	. . . . . . . . 9 ⊢ Ⅎ𝑥∅ ∈ 𝑦
25		nfra1 2469	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦
26	24, 25	nfan 1545	. . . . . . . 8 ⊢ Ⅎ𝑥(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
27	26	nfsab 2132	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
28	23, 27	nfan 1545	. . . . . 6 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})
29		nfcvd 2283	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → Ⅎ𝑥𝐴)
30		nfvd 1510	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → Ⅎ𝑥(𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
31	2, 7, 22, 28, 29, 30	vtocldf 2740	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
32	31	ralrimiva 2508	. . . 4 ⊢ (𝐴 ∈ V → ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
33		ralim 2494	. . . . 5 ⊢ (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧) → (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}𝐴 ∈ 𝑧 → ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧))
34		elintg 3787	. . . . . 6 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}𝐴 ∈ 𝑧))
35		sucexg 4422	. . . . . . 7 ⊢ (𝐴 ∈ V → suc 𝐴 ∈ V)
36		elintg 3787	. . . . . . 7 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧))
37	35, 36	syl 14	. . . . . 6 ⊢ (𝐴 ∈ V → (suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧))
38	34, 37	imbi12d 233	. . . . 5 ⊢ (𝐴 ∈ V → ((𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) ↔ (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}𝐴 ∈ 𝑧 → ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧)))
39	33, 38	syl5ibr 155	. . . 4 ⊢ (𝐴 ∈ V → (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧) → (𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})))
40	32, 39	mpd 13	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}))
41		dfom3 4514	. . . 4 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
42	41	eleq2i 2207	. . 3 ⊢ (𝐴 ∈ ω ↔ 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})
43	41	eleq2i 2207	. . 3 ⊢ (suc 𝐴 ∈ ω ↔ suc 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})
44	40, 42, 43	3imtr4g 204	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ω → suc 𝐴 ∈ ω))
45	1, 44	mpcom 36	1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1330   = wceq 1332   ∈ wcel 1481  [wsb 1736  {cab 2126  ∀wral 2417  Vcvv 2689  ∅c0 3368  ∩ cint 3779  suc csuc 4295  ωcom 4512

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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-uni 3745  df-int 3780  df-suc 4301  df-iom 4513

This theorem is referenced by:  peano5  4520  limom  4535  peano2b  4536  nnregexmid  4542  omsinds  4543  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecrdg  6313  nnacl  6384  nnacom  6388  nnmsucr  6392  nnsucsssuc  6396  nnaword  6415  1onn  6424  2onn  6425  3onn  6426  4onn  6427  nnaordex  6431  php5  6760  phplem4dom  6764  php5dom  6765  phplem4on  6769  dif1en  6781  findcard  6790  findcard2  6791  findcard2s  6792  infnfi  6797  unsnfi  6815  omp1eomlem  6987  ctmlemr  7001  infnninf  7030  nnnninf  7031  frec2uzrand  10209  frecuzrdgsuc  10218  frecuzrdgsuctlem  10227  frecfzennn  10230  hashunlem  10582  ennnfonelemk  11949  ennnfonelemg  11952  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemrn  11968  ennnfonelemnn0  11971  ctinfomlemom  11976  0nninf  13372  nnsf  13374  peano4nninf  13375  nninfalllemn  13377  nninfsellemdc  13381  nninfsellemsuc  13383  nninfself  13384  nninfsellemeqinf  13387