Theorem peano2 4606

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 2760	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ V)
2		simpl 109	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → 𝐴 ∈ V)
3		eleq1 2250	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝐴 ∈ 𝑧))
4		suceq 4414	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → suc 𝑥 = suc 𝐴)
5	4	eleq1d 2256	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (suc 𝑥 ∈ 𝑧 ↔ suc 𝐴 ∈ 𝑧))
6	3, 5	imbi12d 234	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧) ↔ (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧)))
7	6	adantl 277	. . . . . 6 ⊢ (((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) ∧ 𝑥 = 𝐴) → ((𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧) ↔ (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧)))
8		df-clab 2174	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
9		simpr 110	. . . . . . . . . . . 12 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
10		df-ral 2470	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦 ↔ ∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
11	9, 10	sylib 122	. . . . . . . . . . 11 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
12	11	sbimi 1774	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦))
13		sbim 1963	. . . . . . . . . . . 12 ⊢ ([𝑧 / 𝑦](𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ ([𝑧 / 𝑦]𝑥 ∈ 𝑦 → [𝑧 / 𝑦]suc 𝑥 ∈ 𝑦))
14		clelsb2 2293	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑦]𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧)
15		clelsb2 2293	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑦]suc 𝑥 ∈ 𝑦 ↔ suc 𝑥 ∈ 𝑧)
16	14, 15	imbi12i 239	. . . . . . . . . . . 12 ⊢ (([𝑧 / 𝑦]𝑥 ∈ 𝑦 → [𝑧 / 𝑦]suc 𝑥 ∈ 𝑦) ↔ (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
17	13, 16	bitri 184	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑦](𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
18	17	sbalv 2015	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑦]∀𝑥(𝑥 ∈ 𝑦 → suc 𝑥 ∈ 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
19	12, 18	sylib 122	. . . . . . . . 9 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
20	8, 19	sylbi 121	. . . . . . . 8 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∀𝑥(𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
21	20	19.21bi 1568	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
22	21	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → (𝑥 ∈ 𝑧 → suc 𝑥 ∈ 𝑧))
23		nfv 1538	. . . . . . 7 ⊢ Ⅎ𝑥 𝐴 ∈ V
24		nfv 1538	. . . . . . . . 9 ⊢ Ⅎ𝑥∅ ∈ 𝑦
25		nfra1 2518	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦
26	24, 25	nfan 1575	. . . . . . . 8 ⊢ Ⅎ𝑥(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
27	26	nfsab 2179	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
28	23, 27	nfan 1575	. . . . . 6 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})
29		nfcvd 2330	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → Ⅎ𝑥𝐴)
30		nfvd 1539	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → Ⅎ𝑥(𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
31	2, 7, 22, 28, 29, 30	vtocldf 2800	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) → (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
32	31	ralrimiva 2560	. . . 4 ⊢ (𝐴 ∈ V → ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧))
33		ralim 2546	. . . . 5 ⊢ (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} (𝐴 ∈ 𝑧 → suc 𝐴 ∈ 𝑧) → (∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}𝐴 ∈ 𝑧 → ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}suc 𝐴 ∈ 𝑧))
34		elintg 3864	. . . . . 6 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}𝐴 ∈ 𝑧))
35		sucexg 4509	. . . . . . 7 ⊢ (𝐴 ∈ V → suc 𝐴 ∈ V)
36		elintg 3864	. . . . . . 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 4603	. . . 4 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
42	41	eleq2i 2254	. . 3 ⊢ (𝐴 ∈ ω ↔ 𝐴 ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)})
43	41	eleq2i 2254	. . 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 1361   = wceq 1363  [wsb 1772   ∈ wcel 2158  {cab 2173  ∀wral 2465  Vcvv 2749  ∅c0 3434  ∩ cint 3856  suc csuc 4377  ωcom 4601

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-un 4445

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-v 2751  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-uni 3822  df-int 3857  df-suc 4383  df-iom 4602

This theorem is referenced by:  peano5  4609  limom  4625  peano2b  4626  nnregexmid  4632  omsinds  4633  freccllem  6417  frecfcllem  6419  frecsuclem  6421  frecrdg  6423  nnacl  6495  nnacom  6499  nnmsucr  6503  nnsucsssuc  6507  nnaword  6526  1onn  6535  2onn  6536  3onn  6537  4onn  6538  nnaordex  6543  php5  6872  phplem4dom  6876  php5dom  6877  phplem4on  6881  dif1en  6893  findcard  6902  findcard2  6903  findcard2s  6904  infnfi  6909  unsnfi  6932  omp1eomlem  7107  ctmlemr  7121  infnninf  7136  infnninfOLD  7137  nnnninf  7138  nnnninfeq  7140  nninfwlpoimlemg  7187  nninfwlpoimlemginf  7188  frec2uzrand  10419  frecuzrdgsuc  10428  frecuzrdgsuctlem  10437  frecfzennn  10440  hashunlem  10798  ennnfonelemk  12415  ennnfonelemg  12418  ennnfonelemkh  12427  ennnfonelemhf1o  12428  ennnfonelemex  12429  ennnfonelemrn  12434  ennnfonelemnn0  12437  ctinfomlemom  12442  0nninf  15050  nnsf  15051  peano4nninf  15052  nninfsellemdc  15056  nninfsellemsuc  15058  nninfself  15059  nninfsellemeqinf  15062