ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  peano2 Unicode version

Theorem peano2 4717
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.
StepHypRef Expression
1 elex 2825 . 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 2295 . . . . . . . 8  |-  ( x  =  A  ->  (
x  e.  z  <->  A  e.  z ) )
4 suceq 4523 . . . . . . . . 9  |-  ( x  =  A  ->  suc  x  =  suc  A )
54eleq1d 2301 . . . . . . . 8  |-  ( x  =  A  ->  ( suc  x  e.  z  <->  suc  A  e.  z ) )
63, 5imbi12d 234 . . . . . . 7  |-  ( x  =  A  ->  (
( x  e.  z  ->  suc  x  e.  z )  <->  ( A  e.  z  ->  suc  A  e.  z ) ) )
76adantl 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 2219 . . . . . . . . 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 2525 . . . . . . . . . . . 12  |-  ( A. x  e.  y  suc  x  e.  y  <->  A. x
( x  e.  y  ->  suc  x  e.  y ) )
119, 10sylib 122 . . . . . . . . . . 11  |-  ( (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  A. x ( x  e.  y  ->  suc  x  e.  y )
)
1211sbimi 1813 . . . . . . . . . 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 2007 . . . . . . . . . . . 12  |-  ( [ z  /  y ] ( x  e.  y  ->  suc  x  e.  y )  <->  ( [
z  /  y ] x  e.  y  ->  [ z  /  y ] suc  x  e.  y ) )
14 clelsb2 2338 . . . . . . . . . . . . 13  |-  ( [ z  /  y ] x  e.  y  <->  x  e.  z )
15 clelsb2 2338 . . . . . . . . . . . . 13  |-  ( [ z  /  y ] suc  x  e.  y  <->  suc  x  e.  z )
1614, 15imbi12i 239 . . . . . . . . . . . 12  |-  ( ( [ z  /  y ] x  e.  y  ->  [ z  /  y ] suc  x  e.  y )  <->  ( x  e.  z  ->  suc  x  e.  z ) )
1713, 16bitri 184 . . . . . . . . . . 11  |-  ( [ z  /  y ] ( x  e.  y  ->  suc  x  e.  y )  <->  ( x  e.  z  ->  suc  x  e.  z ) )
1817sbalv 2059 . . . . . . . . . 10  |-  ( [ z  /  y ] A. x ( x  e.  y  ->  suc  x  e.  y )  <->  A. x ( x  e.  z  ->  suc  x  e.  z ) )
1912, 18sylib 122 . . . . . . . . 9  |-  ( [ z  /  y ] ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  A. x
( x  e.  z  ->  suc  x  e.  z ) )
208, 19sylbi 121 . . . . . . . 8  |-  ( z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  A. x
( x  e.  z  ->  suc  x  e.  z ) )
212019.21bi 1607 . . . . . . 7  |-  ( z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  (
x  e.  z  ->  suc  x  e.  z ) )
2221adantl 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 1577 . . . . . . 7  |-  F/ x  A  e.  _V
24 nfv 1577 . . . . . . . . 9  |-  F/ x (/) 
e.  y
25 nfra1 2573 . . . . . . . . 9  |-  F/ x A. x  e.  y  suc  x  e.  y
2624, 25nfan 1614 . . . . . . . 8  |-  F/ x
( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )
2726nfsab 2224 . . . . . . 7  |-  F/ x  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
2823, 27nfan 1614 . . . . . 6  |-  F/ x
( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
29 nfcvd 2385 . . . . . 6  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  F/_ x A )
30 nfvd 1578 . . . . . 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 ) )
312, 7, 22, 28, 29, 30vtocldf 2866 . . . . 5  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  ( A  e.  z  ->  suc  A  e.  z ) )
3231ralrimiva 2615 . . . 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 2601 . . . . 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 3957 . . . . . 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 4620 . . . . . . 7  |-  ( A  e.  _V  ->  suc  A  e.  _V )
36 elintg 3957 . . . . . . 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 ) )
3735, 36syl 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 ) )
3834, 37imbi12d 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 ) ) )
3933, 38imbitrrid 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 ) } ) ) )
4032, 39mpd 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 4714 . . . 4  |-  om  =  |^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
4241eleq2i 2299 . . 3  |-  ( A  e.  om  <->  A  e.  |^|
{ y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
4341eleq2i 2299 . . 3  |-  ( suc 
A  e.  om  <->  suc  A  e. 
|^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
4440, 42, 433imtr4g 205 . 2  |-  ( A  e.  _V  ->  ( A  e.  om  ->  suc 
A  e.  om )
)
451, 44mpcom 36 1  |-  ( A  e.  om  ->  suc  A  e.  om )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105   A.wal 1396    = wceq 1398   [wsb 1811    e. wcel 2203   {cab 2218   A.wral 2520   _Vcvv 2813   (/)c0 3508   |^|cint 3949   suc csuc 4486   omcom 4712
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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554
This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-uni 3915  df-int 3950  df-suc 4492  df-iom 4713
This theorem is referenced by:  peano5  4720  limom  4736  peano2b  4737  nnregexmid  4743  omsinds  4744  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecrdg  6639  nnacl  6713  nnacom  6717  nnmsucr  6721  nnsucsssuc  6725  nnaword  6744  1onn  6753  2onn  6754  3onn  6755  4onn  6756  nnaordex  6761  php5  7112  phplem4dom  7116  php5dom  7117  phplem4on  7122  dif1en  7136  findcard  7145  findcard2  7146  findcard2s  7147  infnfi  7152  unsnfi  7179  omp1eomlem  7385  ctmlemr  7399  nninfninc  7414  infnninf  7415  infnninfOLD  7416  nnnninf  7417  nnnninfeq  7419  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  frec2uzrand  10767  frecuzrdgsuc  10776  frecuzrdgsuctlem  10785  frecfzennn  10788  hashunlem  11168  ennnfonelemk  13151  ennnfonelemg  13154  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemrn  13170  ennnfonelemnn0  13173  ctinfomlemom  13178  0nninf  16782  nnsf  16783  peano4nninf  16784  nninfsellemdc  16788  nninfsellemsuc  16790  nninfself  16791  nninfsellemeqinf  16794  nnnninfex  16800
  Copyright terms: Public domain W3C validator