Theorem finds 4472

Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. This is Metamath 100 proof #74. (Contributed by NM, 14-Apr-1995.)

Hypotheses

Ref	Expression
finds.1	|- ( x = (/) -> ( ph <-> ps ) )
finds.2	|- ( x = y -> ( ph <-> ch ) )
finds.3	|- ( x = suc y -> ( ph <-> th ) )
finds.4	|- ( x = A -> ( ph <-> ta ) )
finds.5	|- ps
finds.6	|- ( y e. om -> ( ch -> th ) )

Assertion

Ref	Expression
finds	|- ( A e. om -> 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 finds

Step	Hyp	Ref	Expression
1		finds.5	. . . . 5 |- ps
2		0ex 4013	. . . . . 6 |- (/) e. _V
3		finds.1	. . . . . 6 |- ( x = (/) -> ( ph <-> ps ) )
4	2, 3	elab 2796	. . . . 5 |- ( (/) e. { x | ph } <-> ps )
5	1, 4	mpbir 145	. . . 4 |- (/) e. { x | ph }
6		finds.6	. . . . . 6 |- ( y e. om -> ( ch -> th ) )
7		vex 2658	. . . . . . 7 |- y e. _V
8		finds.2	. . . . . . 7 |- ( x = y -> ( ph <-> ch ) )
9	7, 8	elab 2796	. . . . . 6 |- ( y e. { x | ph } <-> ch )
10	7	sucex 4373	. . . . . . 7 |- suc y e. _V
11		finds.3	. . . . . . 7 |- ( x = suc y -> ( ph <-> th ) )
12	10, 11	elab 2796	. . . . . 6 |- ( suc y e. { x | ph } <-> th )
13	6, 9, 12	3imtr4g 204	. . . . 5 |- ( y e. om -> ( y e. { x | ph } -> suc y e. { x | ph } ) )
14	13	rgen 2457	. . . 4 |- A. y e. om ( y e. { x | ph } -> suc y e. { x | ph } )
15		peano5 4470	. . . 4 |- ( ( (/) e. { x | ph } /\ A. y e. om ( y e. { x | ph } -> suc y e. { x | ph } ) ) -> om C_ { x | ph } )
16	5, 14, 15	mp2an 420	. . 3 |- om C_ { x | ph }
17	16	sseli 3057	. 2 |- ( A e. om -> A e. { x | ph } )
18		finds.4	. . 3 |- ( x = A -> ( ph <-> ta ) )
19	18	elabg 2797	. 2 |- ( A e. om -> ( A e. { x | ph } <-> ta ) )
20	17, 19	mpbid 146	1 |- ( A e. om -> ta )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1312   e. wcel 1461   {cab 2099   A.wral 2388   C_ wss 3035   (/)c0 3327   suc csuc 4245   omcom 4462

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-iinf 4460

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-pw 3476  df-sn 3497  df-pr 3498  df-uni 3701  df-int 3736  df-suc 4251  df-iom 4463

This theorem is referenced by:  findes  4475  nn0suc  4476  elnn  4477  ordom  4478  nndceq0  4489  0elnn  4490  omsinds  4493  nna0r  6326  nnm0r  6327  nnsucelsuc  6339  nneneq  6702  php5  6703  php5dom  6708  fidcenumlemrk  6792  fidcenumlemr  6793  frec2uzltd  10063  frecuzrdgg  10076  seq3val  10118  seqvalcd  10119  omgadd  10435  zfz1iso  10471  ennnfonelemhom  11767  nninfalllemn  12883  nninfsellemdc  12887