Theorem peano2 4615

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 2763	. 2 |- ( A e. om -> A e. _V )
2		simpl 109	. . . . . 6 |- ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) -> A e. _V )
3		eleq1 2252	. . . . . . . 8 |- ( x = A -> ( x e. z <-> A e. z ) )
4		suceq 4423	. . . . . . . . 9 |- ( x = A -> suc x = suc A )
5	4	eleq1d 2258	. . . . . . . 8 |- ( x = A -> ( suc x e. z <-> suc A e. z ) )
6	3, 5	imbi12d 234	. . . . . . 7 |- ( x = A -> ( ( x e. z -> suc x e. z ) <-> ( A e. z -> suc A e. z ) ) )
7	6	adantl 277	. . . . . 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 2176	. . . . . . . . 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 110	. . . . . . . . . . . 12 |- ( ( (/) e. y /\ A. x e. y suc x e. y ) -> A. x e. y suc x e. y )
10		df-ral 2473	. . . . . . . . . . . 12 |- ( A. x e. y suc x e. y <-> A. x ( x e. y -> suc x e. y ) )
11	9, 10	sylib 122	. . . . . . . . . . 11 |- ( ( (/) e. y /\ A. x e. y suc x e. y ) -> A. x ( x e. y -> suc x e. y ) )
12	11	sbimi 1775	. . . . . . . . . 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 1965	. . . . . . . . . . . 12 |- ( [ z / y ] ( x e. y -> suc x e. y ) <-> ( [ z / y ] x e. y -> [ z / y ] suc x e. y ) )
14		clelsb2 2295	. . . . . . . . . . . . 13 |- ( [ z / y ] x e. y <-> x e. z )
15		clelsb2 2295	. . . . . . . . . . . . 13 |- ( [ z / y ] suc x e. y <-> suc x e. z )
16	14, 15	imbi12i 239	. . . . . . . . . . . 12 |- ( ( [ z / y ] x e. y -> [ z / y ] suc x e. y ) <-> ( x e. z -> suc x e. z ) )
17	13, 16	bitri 184	. . . . . . . . . . 11 |- ( [ z / y ] ( x e. y -> suc x e. y ) <-> ( x e. z -> suc x e. z ) )
18	17	sbalv 2017	. . . . . . . . . 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 122	. . . . . . . . 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 121	. . . . . . . 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 1569	. . . . . . 7 |- ( z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> ( x e. z -> suc x e. z ) )
22	21	adantl 277	. . . . . 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 1539	. . . . . . 7 |- F/ x A e. _V
24		nfv 1539	. . . . . . . . 9 |- F/ x (/) e. y
25		nfra1 2521	. . . . . . . . 9 |- F/ x A. x e. y suc x e. y
26	24, 25	nfan 1576	. . . . . . . 8 |- F/ x ( (/) e. y /\ A. x e. y suc x e. y )
27	26	nfsab 2181	. . . . . . 7 |- F/ x z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
28	23, 27	nfan 1576	. . . . . 6 |- F/ x ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } )
29		nfcvd 2333	. . . . . 6 |- ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) -> F/_ x A )
30		nfvd 1540	. . . . . 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 2803	. . . . 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 2563	. . . 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 2549	. . . . 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 3870	. . . . . 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 4518	. . . . . . 7 |- ( A e. _V -> suc A e. _V )
36		elintg 3870	. . . . . . 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 234	. . . . 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	imbitrrid 156	. . . 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 4612	. . . 4 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
42	41	eleq2i 2256	. . 3 |- ( A e. om <-> A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } )
43	41	eleq2i 2256	. . 3 |- ( suc A e. om <-> suc A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } )
44	40, 42, 43	3imtr4g 205	. 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 104   <-> wb 105   A.wal 1362   = wceq 1364   [wsb 1773   e. wcel 2160   {cab 2175   A.wral 2468   _Vcvv 2752   (/)c0 3437   |^|cint 3862   suc csuc 4386   omcom 4610

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4139  ax-pow 4195  ax-pr 4230  ax-un 4454

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-uni 3828  df-int 3863  df-suc 4392  df-iom 4611

This theorem is referenced by:  peano5  4618  limom  4634  peano2b  4635  nnregexmid  4641  omsinds  4642  freccllem  6431  frecfcllem  6433  frecsuclem  6435  frecrdg  6437  nnacl  6509  nnacom  6513  nnmsucr  6517  nnsucsssuc  6521  nnaword  6540  1onn  6549  2onn  6550  3onn  6551  4onn  6552  nnaordex  6557  php5  6890  phplem4dom  6894  php5dom  6895  phplem4on  6899  dif1en  6911  findcard  6920  findcard2  6921  findcard2s  6922  infnfi  6927  unsnfi  6951  omp1eomlem  7127  ctmlemr  7141  nninfninc  7156  infnninf  7157  infnninfOLD  7158  nnnninf  7159  nnnninfeq  7161  nninfwlpoimlemg  7208  nninfwlpoimlemginf  7209  frec2uzrand  10443  frecuzrdgsuc  10452  frecuzrdgsuctlem  10461  frecfzennn  10464  hashunlem  10826  ennnfonelemk  12463  ennnfonelemg  12466  ennnfonelemkh  12475  ennnfonelemhf1o  12476  ennnfonelemex  12477  ennnfonelemrn  12482  ennnfonelemnn0  12485  ctinfomlemom  12490  0nninf  15258  nnsf  15259  peano4nninf  15260  nninfsellemdc  15264  nninfsellemsuc  15266  nninfself  15267  nninfsellemeqinf  15270