Theorem peano2 4644

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 2783	. 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 2268	. . . . . . . 8 |- ( x = A -> ( x e. z <-> A e. z ) )
4		suceq 4450	. . . . . . . . 9 |- ( x = A -> suc x = suc A )
5	4	eleq1d 2274	. . . . . . . 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 2192	. . . . . . . . 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 2489	. . . . . . . . . . . 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 1787	. . . . . . . . . 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 1981	. . . . . . . . . . . 12 |- ( [ z / y ] ( x e. y -> suc x e. y ) <-> ( [ z / y ] x e. y -> [ z / y ] suc x e. y ) )
14		clelsb2 2311	. . . . . . . . . . . . 13 |- ( [ z / y ] x e. y <-> x e. z )
15		clelsb2 2311	. . . . . . . . . . . . 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 2033	. . . . . . . . . 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 1581	. . . . . . 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 1551	. . . . . . 7 |- F/ x A e. _V
24		nfv 1551	. . . . . . . . 9 |- F/ x (/) e. y
25		nfra1 2537	. . . . . . . . 9 |- F/ x A. x e. y suc x e. y
26	24, 25	nfan 1588	. . . . . . . 8 |- F/ x ( (/) e. y /\ A. x e. y suc x e. y )
27	26	nfsab 2197	. . . . . . 7 |- F/ x z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
28	23, 27	nfan 1588	. . . . . 6 |- F/ x ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } )
29		nfcvd 2349	. . . . . 6 |- ( ( A e. _V /\ z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } ) -> F/_ x A )
30		nfvd 1552	. . . . . 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 2824	. . . . 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 2579	. . . 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 2565	. . . . 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 3893	. . . . . 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 4547	. . . . . . 7 |- ( A e. _V -> suc A e. _V )
36		elintg 3893	. . . . . . 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 4641	. . . 4 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
42	41	eleq2i 2272	. . 3 |- ( A e. om <-> A e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } )
43	41	eleq2i 2272	. . 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 1371   = wceq 1373   [wsb 1785   e. wcel 2176   {cab 2191   A.wral 2484   _Vcvv 2772   (/)c0 3460   |^|cint 3885   suc csuc 4413   omcom 4639

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254  ax-un 4481

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-uni 3851  df-int 3886  df-suc 4419  df-iom 4640

This theorem is referenced by:  peano5  4647  limom  4663  peano2b  4664  nnregexmid  4670  omsinds  4671  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecrdg  6496  nnacl  6568  nnacom  6572  nnmsucr  6576  nnsucsssuc  6580  nnaword  6599  1onn  6608  2onn  6609  3onn  6610  4onn  6611  nnaordex  6616  php5  6957  phplem4dom  6961  php5dom  6962  phplem4on  6966  dif1en  6978  findcard  6987  findcard2  6988  findcard2s  6989  infnfi  6994  unsnfi  7018  omp1eomlem  7198  ctmlemr  7212  nninfninc  7227  infnninf  7228  infnninfOLD  7229  nnnninf  7230  nnnninfeq  7232  nninfwlpoimlemg  7279  nninfwlpoimlemginf  7280  frec2uzrand  10552  frecuzrdgsuc  10561  frecuzrdgsuctlem  10570  frecfzennn  10573  hashunlem  10951  ennnfonelemk  12804  ennnfonelemg  12807  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemex  12818  ennnfonelemrn  12823  ennnfonelemnn0  12826  ctinfomlemom  12831  0nninf  15978  nnsf  15979  peano4nninf  15980  nninfsellemdc  15984  nninfsellemsuc  15986  nninfself  15987  nninfsellemeqinf  15990  nnnninfex  15996