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

Theorem indpi 6326
Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)
Hypotheses
Ref Expression
indpi.1  1o
indpi.2
indpi.3  +N  1o
indpi.4
indpi.5
indpi.6  N.
Assertion
Ref Expression
indpi  N.
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()

Proof of Theorem indpi
StepHypRef Expression
1 indpi.4 . 2
2 elni 6292 . . 3  N.  om  =/=  (/)
3 eqid 2037 . . . . . . . . . 10  (/)  (/)
43orci 649 . . . . . . . . 9  (/)  (/)  [. (/)  ].
5 nfv 1418 . . . . . . . . . . 11  F/ (/)  (/)
6 nfsbc1v 2776 . . . . . . . . . . 11  F/ [. (/)  ].
75, 6nfor 1463 . . . . . . . . . 10  F/ (/)  (/)  [. (/)  ].
8 0ex 3875 . . . . . . . . . 10  (/)  _V
9 eqeq1 2043 . . . . . . . . . . 11  (/)  (/)  (/)  (/)
10 sbceq1a 2767 . . . . . . . . . . 11  (/) 
[. (/)  ].
119, 10orbi12d 706 . . . . . . . . . 10  (/)  (/)  (/)  (/)  [. (/)  ].
127, 8, 11elabf 2680 . . . . . . . . 9  (/)  {  |  (/)  }  (/)  (/) 
[. (/)  ].
134, 12mpbir 134 . . . . . . . 8  (/)  {  |  (/)  }
14 suceq 4105 . . . . . . . . . . . . . 14  (/)  suc  suc  (/)
15 df-1o 5940 . . . . . . . . . . . . . 14  1o  suc  (/)
1614, 15syl6eqr 2087 . . . . . . . . . . . . 13  (/)  suc  1o
17 indpi.5 . . . . . . . . . . . . . . 15
1817olci 650 . . . . . . . . . . . . . 14  1o  (/)
19 1onn 6029 . . . . . . . . . . . . . . . 16  1o  om
2019elexi 2561 . . . . . . . . . . . . . . 15  1o  _V
21 eqeq1 2043 . . . . . . . . . . . . . . . 16  1o  (/)  1o  (/)
22 indpi.1 . . . . . . . . . . . . . . . 16  1o
2321, 22orbi12d 706 . . . . . . . . . . . . . . 15  1o  (/)  1o  (/)
2420, 23elab 2681 . . . . . . . . . . . . . 14  1o  {  |  (/)  }  1o  (/)
2518, 24mpbir 134 . . . . . . . . . . . . 13  1o  {  |  (/)  }
2616, 25syl6eqel 2125 . . . . . . . . . . . 12  (/)  suc  {  |  (/)  }
2726a1d 22 . . . . . . . . . . 11  (/)  {  |  (/)  }  suc  {  |  (/)  }
2827a1i 9 . . . . . . . . . 10  om  (/)  {  |  (/)  }  suc  {  |  (/)  }
29 indpi.6 . . . . . . . . . . . 12  N.
30 elni 6292 . . . . . . . . . . . . . . . 16  N.  om  =/=  (/)
3130simprbi 260 . . . . . . . . . . . . . . 15  N.  =/=  (/)
3231neneqd 2221 . . . . . . . . . . . . . 14  N.  (/)
33 biorf 662 . . . . . . . . . . . . . 14  (/)  (/)
3432, 33syl 14 . . . . . . . . . . . . 13  N.  (/)
35 vex 2554 . . . . . . . . . . . . . 14 
_V
36 eqeq1 2043 . . . . . . . . . . . . . . 15  (/)  (/)
37 indpi.2 . . . . . . . . . . . . . . 15
3836, 37orbi12d 706 . . . . . . . . . . . . . 14  (/)  (/)
3935, 38elab 2681 . . . . . . . . . . . . 13  {  |  (/)  }  (/)
4034, 39syl6bbr 187 . . . . . . . . . . . 12  N.  {  |  (/)  }
41 1pi 6299 . . . . . . . . . . . . . . . . . 18  1o  N.
42 addclpi 6311 . . . . . . . . . . . . . . . . . 18  N.  1o  N.  +N  1o  N.
4341, 42mpan2 401 . . . . . . . . . . . . . . . . 17  N.  +N  1o 
N.
44 elni 6292 . . . . . . . . . . . . . . . . 17  +N  1o  N.  +N  1o  om  +N  1o  =/=  (/)
4543, 44sylib 127 . . . . . . . . . . . . . . . 16  N.  +N  1o  om  +N  1o  =/=  (/)
4645simprd 107 . . . . . . . . . . . . . . 15  N.  +N  1o  =/=  (/)
4746neneqd 2221 . . . . . . . . . . . . . 14  N.  +N  1o  (/)
48 biorf 662 . . . . . . . . . . . . . 14  +N  1o  (/)  +N  1o  (/)
4947, 48syl 14 . . . . . . . . . . . . 13  N.  +N  1o  (/)
50 eqeq1 2043 . . . . . . . . . . . . . . . 16  +N  1o  (/)  +N  1o  (/)
51 indpi.3 . . . . . . . . . . . . . . . 16  +N  1o
5250, 51orbi12d 706 . . . . . . . . . . . . . . 15  +N  1o  (/)  +N  1o  (/)
5352elabg 2682 . . . . . . . . . . . . . 14  +N  1o  N.  +N  1o  {  |  (/)  }  +N  1o  (/)
5443, 53syl 14 . . . . . . . . . . . . 13  N.  +N  1o  {  |  (/)  }  +N  1o  (/)
55 addpiord 6300 . . . . . . . . . . . . . . . 16  N.  1o  N.  +N  1o  +o  1o
5641, 55mpan2 401 . . . . . . . . . . . . . . 15  N.  +N  1o  +o  1o
57 pion 6294 . . . . . . . . . . . . . . . 16  N.  On
58 oa1suc 5986 . . . . . . . . . . . . . . . 16  On  +o  1o 
suc
5957, 58syl 14 . . . . . . . . . . . . . . 15  N.  +o  1o 
suc
6056, 59eqtrd 2069 . . . . . . . . . . . . . 14  N.  +N  1o 
suc
6160eleq1d 2103 . . . . . . . . . . . . 13  N.  +N  1o  {  |  (/)  }  suc  {  |  (/)  }
6249, 54, 613bitr2d 205 . . . . . . . . . . . 12  N.  suc  {  |  (/)  }
6329, 40, 623imtr3d 191 . . . . . . . . . . 11  N.  {  |  (/)  }  suc  {  |  (/)  }
6463a1i 9 . . . . . . . . . 10  om  N.  {  |  (/)  }  suc  {  |  (/)  }
65 nndceq0 4282 . . . . . . . . . . . 12  om DECID  (/)
66 df-dc 742 . . . . . . . . . . . 12 DECID  (/)  (/)  (/)
6765, 66sylib 127 . . . . . . . . . . 11  om  (/)  (/)
68 idd 21 . . . . . . . . . . . . . . 15  om  (/)  (/)
6968necon3bd 2242 . . . . . . . . . . . . . 14  om  (/)  =/=  (/)
7069anc2li 312 . . . . . . . . . . . . 13  om  (/)  om  =/=  (/)
7170, 30syl6ibr 151 . . . . . . . . . . . 12  om  (/)  N.
7271orim2d 701 . . . . . . . . . . 11  om  (/)  (/)  (/)  N.
7367, 72mpd 13 . . . . . . . . . 10  om  (/)  N.
7428, 64, 73mpjaod 637 . . . . . . . . 9  om  {  |  (/)  }  suc  {  |  (/)  }
7574rgen 2368 . . . . . . . 8  om 
{  |  (/)  }  suc  {  |  (/)  }
76 peano5 4264 . . . . . . . 8  (/)  {  |  (/)  }  om 
{  |  (/)  }  suc  {  |  (/)  }  om  C_  {  |  (/)  }
7713, 75, 76mp2an 402 . . . . . . 7  om  C_  {  |  (/)  }
7877sseli 2935 . . . . . 6  om  {  |  (/)  }
79 abid 2025 . . . . . 6  {  |  (/)  }  (/)
8078, 79sylib 127 . . . . 5  om  (/)
8180adantr 261 . . . 4  om  =/=  (/)  (/)
82 df-ne 2203 . . . . . 6  =/=  (/)  (/)
83 biorf 662 . . . . . 6  (/)  (/)
8482, 83sylbi 114 . . . . 5  =/=  (/)  (/)
8584adantl 262 . . . 4  om  =/=  (/)  (/)
8681, 85mpbird 156 . . 3  om  =/=  (/)
872, 86sylbi 114 . 2  N.
881, 87vtoclga 2613 1  N.
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 97   wb 98   wo 628  DECID wdc 741   wceq 1242   wcel 1390   {cab 2023    =/= wne 2201  wral 2300   [.wsbc 2758    C_ wss 2911   (/)c0 3218   Oncon0 4066   suc csuc 4068   omcom 4256  (class class class)co 5455   1oc1o 5933    +o coa 5937   N.cnpi 6256    +N cpli 6257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-dc 742  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-oadd 5944  df-ni 6288  df-pli 6289
This theorem is referenced by:  pitonn  6744
  Copyright terms: Public domain W3C validator