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

Theorem indpi 7340
Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)
Hypotheses
Ref Expression
indpi.1  |-  ( x  =  1o  ->  ( ph 
<->  ps ) )
indpi.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
indpi.3  |-  ( x  =  ( y  +N  1o )  ->  ( ph 
<->  th ) )
indpi.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
indpi.5  |-  ps
indpi.6  |-  ( y  e.  N.  ->  ( ch  ->  th ) )
Assertion
Ref Expression
indpi  |-  ( A  e.  N.  ->  ta )
Distinct variable groups:    x, y    x, A    ps, x    ch, x    th, x    ta, x    ph, y
Allowed substitution hints:    ph( x)    ps( y)    ch( y)    th( y)    ta( y)    A( y)

Proof of Theorem indpi
StepHypRef Expression
1 indpi.4 . 2  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2 elni 7306 . . 3  |-  ( x  e.  N.  <->  ( x  e.  om  /\  x  =/=  (/) ) )
3 eqid 2177 . . . . . . . . . 10  |-  (/)  =  (/)
43orci 731 . . . . . . . . 9  |-  ( (/)  =  (/)  \/  [. (/)  /  x ]. ph )
5 nfv 1528 . . . . . . . . . . 11  |-  F/ x (/)  =  (/)
6 nfsbc1v 2981 . . . . . . . . . . 11  |-  F/ x [. (/)  /  x ]. ph
75, 6nfor 1574 . . . . . . . . . 10  |-  F/ x
( (/)  =  (/)  \/  [. (/)  /  x ]. ph )
8 0ex 4130 . . . . . . . . . 10  |-  (/)  e.  _V
9 eqeq1 2184 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( x  =  (/)  <->  (/)  =  (/) ) )
10 sbceq1a 2972 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( ph  <->  [. (/)  /  x ]. ph )
)
119, 10orbi12d 793 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( ( x  =  (/)  \/  ph ) 
<->  ( (/)  =  (/)  \/  [. (/)  /  x ]. ph )
) )
127, 8, 11elabf 2880 . . . . . . . . 9  |-  ( (/)  e.  { x  |  ( x  =  (/)  \/  ph ) }  <->  ( (/)  =  (/)  \/ 
[. (/)  /  x ]. ph ) )
134, 12mpbir 146 . . . . . . . 8  |-  (/)  e.  {
x  |  ( x  =  (/)  \/  ph ) }
14 suceq 4402 . . . . . . . . . . . . . 14  |-  ( y  =  (/)  ->  suc  y  =  suc  (/) )
15 df-1o 6416 . . . . . . . . . . . . . 14  |-  1o  =  suc  (/)
1614, 15eqtr4di 2228 . . . . . . . . . . . . 13  |-  ( y  =  (/)  ->  suc  y  =  1o )
17 indpi.5 . . . . . . . . . . . . . . 15  |-  ps
1817olci 732 . . . . . . . . . . . . . 14  |-  ( 1o  =  (/)  \/  ps )
19 1oex 6424 . . . . . . . . . . . . . . 15  |-  1o  e.  _V
20 eqeq1 2184 . . . . . . . . . . . . . . . 16  |-  ( x  =  1o  ->  (
x  =  (/)  <->  1o  =  (/) ) )
21 indpi.1 . . . . . . . . . . . . . . . 16  |-  ( x  =  1o  ->  ( ph 
<->  ps ) )
2220, 21orbi12d 793 . . . . . . . . . . . . . . 15  |-  ( x  =  1o  ->  (
( x  =  (/)  \/ 
ph )  <->  ( 1o  =  (/)  \/  ps )
) )
2319, 22elab 2881 . . . . . . . . . . . . . 14  |-  ( 1o  e.  { x  |  ( x  =  (/)  \/ 
ph ) }  <->  ( 1o  =  (/)  \/  ps )
)
2418, 23mpbir 146 . . . . . . . . . . . . 13  |-  1o  e.  { x  |  ( x  =  (/)  \/  ph ) }
2516, 24eqeltrdi 2268 . . . . . . . . . . . 12  |-  ( y  =  (/)  ->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } )
2625a1d 22 . . . . . . . . . . 11  |-  ( y  =  (/)  ->  ( y  e.  { x  |  ( x  =  (/)  \/ 
ph ) }  ->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } ) )
2726a1i 9 . . . . . . . . . 10  |-  ( y  e.  om  ->  (
y  =  (/)  ->  (
y  e.  { x  |  ( x  =  (/)  \/  ph ) }  ->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } ) ) )
28 indpi.6 . . . . . . . . . . . 12  |-  ( y  e.  N.  ->  ( ch  ->  th ) )
29 elni 7306 . . . . . . . . . . . . . . . 16  |-  ( y  e.  N.  <->  ( y  e.  om  /\  y  =/=  (/) ) )
3029simprbi 275 . . . . . . . . . . . . . . 15  |-  ( y  e.  N.  ->  y  =/=  (/) )
3130neneqd 2368 . . . . . . . . . . . . . 14  |-  ( y  e.  N.  ->  -.  y  =  (/) )
32 biorf 744 . . . . . . . . . . . . . 14  |-  ( -.  y  =  (/)  ->  ( ch 
<->  ( y  =  (/)  \/ 
ch ) ) )
3331, 32syl 14 . . . . . . . . . . . . 13  |-  ( y  e.  N.  ->  ( ch 
<->  ( y  =  (/)  \/ 
ch ) ) )
34 vex 2740 . . . . . . . . . . . . . 14  |-  y  e. 
_V
35 eqeq1 2184 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
x  =  (/)  <->  y  =  (/) ) )
36 indpi.2 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
3735, 36orbi12d 793 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
( x  =  (/)  \/ 
ph )  <->  ( y  =  (/)  \/  ch )
) )
3834, 37elab 2881 . . . . . . . . . . . . 13  |-  ( y  e.  { x  |  ( x  =  (/)  \/ 
ph ) }  <->  ( y  =  (/)  \/  ch )
)
3933, 38bitr4di 198 . . . . . . . . . . . 12  |-  ( y  e.  N.  ->  ( ch 
<->  y  e.  { x  |  ( x  =  (/)  \/  ph ) } ) )
40 1pi 7313 . . . . . . . . . . . . . . . . . 18  |-  1o  e.  N.
41 addclpi 7325 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  N.  /\  1o  e.  N. )  -> 
( y  +N  1o )  e.  N. )
4240, 41mpan2 425 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  N.  ->  (
y  +N  1o )  e.  N. )
43 elni 7306 . . . . . . . . . . . . . . . . 17  |-  ( ( y  +N  1o )  e.  N.  <->  ( (
y  +N  1o )  e.  om  /\  (
y  +N  1o )  =/=  (/) ) )
4442, 43sylib 122 . . . . . . . . . . . . . . . 16  |-  ( y  e.  N.  ->  (
( y  +N  1o )  e.  om  /\  (
y  +N  1o )  =/=  (/) ) )
4544simprd 114 . . . . . . . . . . . . . . 15  |-  ( y  e.  N.  ->  (
y  +N  1o )  =/=  (/) )
4645neneqd 2368 . . . . . . . . . . . . . 14  |-  ( y  e.  N.  ->  -.  ( y  +N  1o )  =  (/) )
47 biorf 744 . . . . . . . . . . . . . 14  |-  ( -.  ( y  +N  1o )  =  (/)  ->  ( th 
<->  ( ( y  +N  1o )  =  (/)  \/ 
th ) ) )
4846, 47syl 14 . . . . . . . . . . . . 13  |-  ( y  e.  N.  ->  ( th 
<->  ( ( y  +N  1o )  =  (/)  \/ 
th ) ) )
49 eqeq1 2184 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( y  +N  1o )  ->  (
x  =  (/)  <->  ( y  +N  1o )  =  (/) ) )
50 indpi.3 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( y  +N  1o )  ->  ( ph 
<->  th ) )
5149, 50orbi12d 793 . . . . . . . . . . . . . . 15  |-  ( x  =  ( y  +N  1o )  ->  (
( x  =  (/)  \/ 
ph )  <->  ( (
y  +N  1o )  =  (/)  \/  th )
) )
5251elabg 2883 . . . . . . . . . . . . . 14  |-  ( ( y  +N  1o )  e.  N.  ->  (
( y  +N  1o )  e.  { x  |  ( x  =  (/)  \/  ph ) }  <-> 
( ( y  +N  1o )  =  (/)  \/ 
th ) ) )
5342, 52syl 14 . . . . . . . . . . . . 13  |-  ( y  e.  N.  ->  (
( y  +N  1o )  e.  { x  |  ( x  =  (/)  \/  ph ) }  <-> 
( ( y  +N  1o )  =  (/)  \/ 
th ) ) )
54 addpiord 7314 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  N.  /\  1o  e.  N. )  -> 
( y  +N  1o )  =  ( y  +o  1o ) )
5540, 54mpan2 425 . . . . . . . . . . . . . . 15  |-  ( y  e.  N.  ->  (
y  +N  1o )  =  ( y  +o  1o ) )
56 pion 7308 . . . . . . . . . . . . . . . 16  |-  ( y  e.  N.  ->  y  e.  On )
57 oa1suc 6467 . . . . . . . . . . . . . . . 16  |-  ( y  e.  On  ->  (
y  +o  1o )  =  suc  y )
5856, 57syl 14 . . . . . . . . . . . . . . 15  |-  ( y  e.  N.  ->  (
y  +o  1o )  =  suc  y )
5955, 58eqtrd 2210 . . . . . . . . . . . . . 14  |-  ( y  e.  N.  ->  (
y  +N  1o )  =  suc  y )
6059eleq1d 2246 . . . . . . . . . . . . 13  |-  ( y  e.  N.  ->  (
( y  +N  1o )  e.  { x  |  ( x  =  (/)  \/  ph ) }  <->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } ) )
6148, 53, 603bitr2d 216 . . . . . . . . . . . 12  |-  ( y  e.  N.  ->  ( th 
<->  suc  y  e.  {
x  |  ( x  =  (/)  \/  ph ) } ) )
6228, 39, 613imtr3d 202 . . . . . . . . . . 11  |-  ( y  e.  N.  ->  (
y  e.  { x  |  ( x  =  (/)  \/  ph ) }  ->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } ) )
6362a1i 9 . . . . . . . . . 10  |-  ( y  e.  om  ->  (
y  e.  N.  ->  ( y  e.  { x  |  ( x  =  (/)  \/  ph ) }  ->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } ) ) )
64 nndceq0 4617 . . . . . . . . . . . 12  |-  ( y  e.  om  -> DECID  y  =  (/) )
65 df-dc 835 . . . . . . . . . . . 12  |-  (DECID  y  =  (/) 
<->  ( y  =  (/)  \/ 
-.  y  =  (/) ) )
6664, 65sylib 122 . . . . . . . . . . 11  |-  ( y  e.  om  ->  (
y  =  (/)  \/  -.  y  =  (/) ) )
67 idd 21 . . . . . . . . . . . . . . 15  |-  ( y  e.  om  ->  (
y  =  (/)  ->  y  =  (/) ) )
6867necon3bd 2390 . . . . . . . . . . . . . 14  |-  ( y  e.  om  ->  ( -.  y  =  (/)  ->  y  =/=  (/) ) )
6968anc2li 329 . . . . . . . . . . . . 13  |-  ( y  e.  om  ->  ( -.  y  =  (/)  ->  (
y  e.  om  /\  y  =/=  (/) ) ) )
7069, 29imbitrrdi 162 . . . . . . . . . . . 12  |-  ( y  e.  om  ->  ( -.  y  =  (/)  ->  y  e.  N. ) )
7170orim2d 788 . . . . . . . . . . 11  |-  ( y  e.  om  ->  (
( y  =  (/)  \/ 
-.  y  =  (/) )  ->  ( y  =  (/)  \/  y  e.  N. ) ) )
7266, 71mpd 13 . . . . . . . . . 10  |-  ( y  e.  om  ->  (
y  =  (/)  \/  y  e.  N. ) )
7327, 63, 72mpjaod 718 . . . . . . . . 9  |-  ( y  e.  om  ->  (
y  e.  { x  |  ( x  =  (/)  \/  ph ) }  ->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } ) )
7473rgen 2530 . . . . . . . 8  |-  A. y  e.  om  ( y  e. 
{ x  |  ( x  =  (/)  \/  ph ) }  ->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } )
75 peano5 4597 . . . . . . . 8  |-  ( (
(/)  e.  { x  |  ( x  =  (/)  \/  ph ) }  /\  A. y  e. 
om  ( y  e. 
{ x  |  ( x  =  (/)  \/  ph ) }  ->  suc  y  e.  { x  |  ( x  =  (/)  \/  ph ) } ) )  ->  om  C_  { x  |  ( x  =  (/)  \/ 
ph ) } )
7613, 74, 75mp2an 426 . . . . . . 7  |-  om  C_  { x  |  ( x  =  (/)  \/  ph ) }
7776sseli 3151 . . . . . 6  |-  ( x  e.  om  ->  x  e.  { x  |  ( x  =  (/)  \/  ph ) } )
78 abid 2165 . . . . . 6  |-  ( x  e.  { x  |  ( x  =  (/)  \/ 
ph ) }  <->  ( x  =  (/)  \/  ph )
)
7977, 78sylib 122 . . . . 5  |-  ( x  e.  om  ->  (
x  =  (/)  \/  ph ) )
8079adantr 276 . . . 4  |-  ( ( x  e.  om  /\  x  =/=  (/) )  ->  (
x  =  (/)  \/  ph ) )
81 df-ne 2348 . . . . . 6  |-  ( x  =/=  (/)  <->  -.  x  =  (/) )
82 biorf 744 . . . . . 6  |-  ( -.  x  =  (/)  ->  ( ph 
<->  ( x  =  (/)  \/ 
ph ) ) )
8381, 82sylbi 121 . . . . 5  |-  ( x  =/=  (/)  ->  ( ph  <->  ( x  =  (/)  \/  ph ) ) )
8483adantl 277 . . . 4  |-  ( ( x  e.  om  /\  x  =/=  (/) )  ->  ( ph 
<->  ( x  =  (/)  \/ 
ph ) ) )
8580, 84mpbird 167 . . 3  |-  ( ( x  e.  om  /\  x  =/=  (/) )  ->  ph )
862, 85sylbi 121 . 2  |-  ( x  e.  N.  ->  ph )
871, 86vtoclga 2803 1  |-  ( A  e.  N.  ->  ta )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 708  DECID wdc 834    = wceq 1353    e. wcel 2148   {cab 2163    =/= wne 2347   A.wral 2455   [.wsbc 2962    C_ wss 3129   (/)c0 3422   Oncon0 4363   suc csuc 4365   omcom 4589  (class class class)co 5874   1oc1o 6409    +o coa 6413   N.cnpi 7270    +N cpli 7271
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-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-iord 4366  df-on 4368  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-1o 6416  df-oadd 6420  df-ni 7302  df-pli 7303
This theorem is referenced by:  pitonn  7846
  Copyright terms: Public domain W3C validator