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

Theorem peano2 4627
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 2771 . 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 2256 . . . . . . . 8  |-  ( x  =  A  ->  (
x  e.  z  <->  A  e.  z ) )
4 suceq 4433 . . . . . . . . 9  |-  ( x  =  A  ->  suc  x  =  suc  A )
54eleq1d 2262 . . . . . . . 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 2180 . . . . . . . . 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 2477 . . . . . . . . . . . 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 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 1969 . . . . . . . . . . . 12  |-  ( [ z  /  y ] ( x  e.  y  ->  suc  x  e.  y )  <->  ( [
z  /  y ] x  e.  y  ->  [ z  /  y ] suc  x  e.  y ) )
14 clelsb2 2299 . . . . . . . . . . . . 13  |-  ( [ z  /  y ] x  e.  y  <->  x  e.  z )
15 clelsb2 2299 . . . . . . . . . . . . 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 2021 . . . . . . . . . 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 1569 . . . . . . 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 1539 . . . . . . 7  |-  F/ x  A  e.  _V
24 nfv 1539 . . . . . . . . 9  |-  F/ x (/) 
e.  y
25 nfra1 2525 . . . . . . . . 9  |-  F/ x A. x  e.  y  suc  x  e.  y
2624, 25nfan 1576 . . . . . . . 8  |-  F/ x
( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )
2726nfsab 2185 . . . . . . 7  |-  F/ x  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
2823, 27nfan 1576 . . . . . 6  |-  F/ x
( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
29 nfcvd 2337 . . . . . 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 ) )
312, 7, 22, 28, 29, 30vtocldf 2811 . . . . 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 2567 . . . 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 2553 . . . . 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 3878 . . . . . 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 4530 . . . . . . 7  |-  ( A  e.  _V  ->  suc  A  e.  _V )
36 elintg 3878 . . . . . . 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 4624 . . . 4  |-  om  =  |^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
4241eleq2i 2260 . . 3  |-  ( A  e.  om  <->  A  e.  |^|
{ y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
4341eleq2i 2260 . . 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 1362    = wceq 1364   [wsb 1773    e. wcel 2164   {cab 2179   A.wral 2472   _Vcvv 2760   (/)c0 3446   |^|cint 3870   suc csuc 4396   omcom 4622
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 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-uni 3836  df-int 3871  df-suc 4402  df-iom 4623
This theorem is referenced by:  peano5  4630  limom  4646  peano2b  4647  nnregexmid  4653  omsinds  4654  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecrdg  6461  nnacl  6533  nnacom  6537  nnmsucr  6541  nnsucsssuc  6545  nnaword  6564  1onn  6573  2onn  6574  3onn  6575  4onn  6576  nnaordex  6581  php5  6914  phplem4dom  6918  php5dom  6919  phplem4on  6923  dif1en  6935  findcard  6944  findcard2  6945  findcard2s  6946  infnfi  6951  unsnfi  6975  omp1eomlem  7153  ctmlemr  7167  nninfninc  7182  infnninf  7183  infnninfOLD  7184  nnnninf  7185  nnnninfeq  7187  nninfwlpoimlemg  7234  nninfwlpoimlemginf  7235  frec2uzrand  10476  frecuzrdgsuc  10485  frecuzrdgsuctlem  10494  frecfzennn  10497  hashunlem  10875  ennnfonelemk  12557  ennnfonelemg  12560  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemrn  12576  ennnfonelemnn0  12579  ctinfomlemom  12584  0nninf  15494  nnsf  15495  peano4nninf  15496  nninfsellemdc  15500  nninfsellemsuc  15502  nninfself  15503  nninfsellemeqinf  15506
  Copyright terms: Public domain W3C validator