Theorem peano2 4552

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	|- ( A e. om -> suc A e. om )

Proof of Theorem peano2

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2723	. 2 |- ( A e. om -> A e. _V )
2		simpl 108	. . . . . 6 |- ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) -> A e. _V )
3		eleq1 2220	. . . . . . . 8 |- ( x = A -> ( x e. z <-> A e. z ) )
4		suceq 4361	. . . . . . . . 9 |- ( x = A -> suc x = suc A )
5	4	eleq1d 2226	. . . . . . . 8 |- ( x = A -> ( suc x e. z <-> suc A e. z ) )
6	3, 5	imbi12d 233	. . . . . . 7 |- ( x = A -> ( ( x e. z -> suc x e. z ) <-> ( A e. z -> suc A e. z ) ) )
7	6	adantl 275	. . . . . 6 |- ( ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) /\ x = A ) -> ( ( x e. z -> suc x e. z ) <-> ( A e. z -> suc A e. z ) ) )
8		df-clab 2144	. . . . . . . . 9 |- ( z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } <-> [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) )
9		simpr 109	. . . . . . . . . . . 12 |- ( ( (/) e. y /\ A. x e. y suc x e. y ) -> A. x e. y suc x e. y )
10		df-ral 2440	. . . . . . . . . . . 12 |- ( A. x e. y suc x e. y <-> A. x ( x e. y -> suc x e. y ) )
11	9, 10	sylib 121	. . . . . . . . . . 11 |- ( ( (/) e. y /\ A. x e. y suc x e. y ) -> A. x ( x e. y -> suc x e. y ) )
12	11	sbimi 1744	. . . . . . . . . 10 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] A. x ( x e. y -> suc x e. y ) )
13		sbim 1933	. . . . . . . . . . . 12 |- ( [ z / y ] ( x e. y -> suc x e. y ) <-> ( [ z / y ] x e. y -> [ z / y ] suc x e. y ) )
14		clelsb4 2263	. . . . . . . . . . . . 13 |- ( [ z / y ] x e. y <-> x e. z )
15		clelsb4 2263	. . . . . . . . . . . . 13 |- ( [ z / y ] suc x e. y <-> suc x e. z )
16	14, 15	imbi12i 238	. . . . . . . . . . . 12 |- ( ( [ z / y ] x e. y -> [ z / y ] suc x e. y ) <-> ( x e. z -> suc x e. z ) )
17	13, 16	bitri 183	. . . . . . . . . . 11 |- ( [ z / y ] ( x e. y -> suc x e. y ) <-> ( x e. z -> suc x e. z ) )
18	17	sbalv 1985	. . . . . . . . . 10 |- ( [ z / y ] A. x ( x e. y -> suc x e. y ) <-> A. x ( x e. z -> suc x e. z ) )
19	12, 18	sylib 121	. . . . . . . . 9 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> A. x ( x e. z -> suc x e. z ) )
20	8, 19	sylbi 120	. . . . . . . 8 |- ( z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> A. x ( x e. z -> suc x e. z ) )
21	20	19.21bi 1538	. . . . . . 7 |- ( z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> ( x e. z -> suc x e. z ) )
22	21	adantl 275	. . . . . 6 |- ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) -> ( x e. z -> suc x e. z ) )
23		nfv 1508	. . . . . . 7 |- F/ x A e. _V
24		nfv 1508	. . . . . . . . 9 |- F/ x (/) e. y
25		nfra1 2488	. . . . . . . . 9 |- F/ x A. x e. y suc x e. y
26	24, 25	nfan 1545	. . . . . . . 8 |- F/ x ( (/) e. y /\ A. x e. y suc x e. y )
27	26	nfsab 2149	. . . . . . 7 |- F/ x z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
28	23, 27	nfan 1545	. . . . . 6 |- F/ x ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } )
29		nfcvd 2300	. . . . . 6 |- ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) -> F/_ x A )
30		nfvd 1509	. . . . . 6 |- ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) -> F/ x ( A e. z -> suc A e. z ) )
31	2, 7, 22, 28, 29, 30	vtocldf 2763	. . . . 5 |- ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) -> ( A e. z -> suc A e. z ) )
32	31	ralrimiva 2530	. . . 4 |- ( A e. _V -> A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ( A e. z -> suc A e. z ) )
33		ralim 2516	. . . . 5 |- ( A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ( A e. z -> suc A e. z ) -> ( A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } A e. z -> A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } suc A e. z ) )
34		elintg 3815	. . . . . 6 |- ( A e. _V -> ( A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } <-> A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } A e. z ) )
35		sucexg 4455	. . . . . . 7 |- ( A e. _V -> suc A e. _V )
36		elintg 3815	. . . . . . 7 |- ( suc A e. _V -> ( suc A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } <-> A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } suc A e. z ) )
37	35, 36	syl 14	. . . . . 6 |- ( A e. _V -> ( suc A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } <-> A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } suc A e. z ) )
38	34, 37	imbi12d 233	. . . . 5 |- ( A e. _V -> ( ( A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> suc A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) <-> ( A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } A e. z -> A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } suc A e. z ) ) )
39	33, 38	syl5ibr 155	. . . 4 |- ( A e. _V -> ( A. z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ( A e. z -> suc A e. z ) -> ( A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> suc A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) ) )
40	32, 39	mpd 13	. . 3 |- ( A e. _V -> ( A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> suc A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) )
41		dfom3 4549	. . . 4 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
42	41	eleq2i 2224	. . 3 |- ( A e. om <-> A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } )
43	41	eleq2i 2224	. . 3 |- ( suc A e. om <-> suc A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } )
44	40, 42, 43	3imtr4g 204	. 2 |- ( A e. _V -> ( A e. om -> suc A e. om ) )
45	1, 44	mpcom 36	1 |- ( A e. om -> suc A e. om )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1333   = wceq 1335   [wsb 1742   e. wcel 2128   {cab 2143   A.wral 2435   _Vcvv 2712   (/)c0 3394   |^|cint 3807   suc csuc 4324   omcom 4547

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 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-sep 4082  ax-pow 4134  ax-pr 4168  ax-un 4392

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-uni 3773  df-int 3808  df-suc 4330  df-iom 4548

This theorem is referenced by:  peano5  4555  limom  4571  peano2b  4572  nnregexmid  4578  omsinds  4579  freccllem  6343  frecfcllem  6345  frecsuclem  6347  frecrdg  6349  nnacl  6420  nnacom  6424  nnmsucr  6428  nnsucsssuc  6432  nnaword  6451  1onn  6460  2onn  6461  3onn  6462  4onn  6463  nnaordex  6467  php5  6796  phplem4dom  6800  php5dom  6801  phplem4on  6805  dif1en  6817  findcard  6826  findcard2  6827  findcard2s  6828  infnfi  6833  unsnfi  6856  omp1eomlem  7028  ctmlemr  7042  infnninf  7056  infnninfOLD  7057  nnnninf  7058  frec2uzrand  10286  frecuzrdgsuc  10295  frecuzrdgsuctlem  10304  frecfzennn  10307  hashunlem  10660  ennnfonelemk  12101  ennnfonelemg  12104  ennnfonelemkh  12113  ennnfonelemhf1o  12114  ennnfonelemex  12115  ennnfonelemrn  12120  ennnfonelemnn0  12123  ctinfomlemom  12128  0nninf  13536  nnsf  13538  peano4nninf  13539  nninfalllemn  13541  nninfsellemdc  13544  nninfsellemsuc  13546  nninfself  13547  nninfsellemeqinf  13550