Theorem finds2 4324

Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 29-Nov-2002.)

Hypotheses

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

Assertion

Ref	Expression
finds2	|- ( x e. om -> ( ta -> ph ) )

Distinct variable groups:   x, y, ta   ps, x   ch, x   th, x   ph, y

Allowed substitution hints:   ph( x)   ps( y)   ch( y)   th( y)

Proof of Theorem finds2

Step	Hyp	Ref	Expression
1		finds2.4	. . . . 5 |- ( ta -> ps )
2		0ex 3884	. . . . . 6 |- (/) e. _V
3		finds2.1	. . . . . . 7 |- ( x = (/) -> ( ph <-> ps ) )
4	3	imbi2d 219	. . . . . 6 |- ( x = (/) -> ( ( ta -> ph ) <-> ( ta -> ps ) ) )
5	2, 4	elab 2687	. . . . 5 |- ( (/) e. { x | ( ta -> ph ) } <-> ( ta -> ps ) )
6	1, 5	mpbir 134	. . . 4 |- (/) e. { x | ( ta -> ph ) }
7		finds2.5	. . . . . . 7 |- ( y e. om -> ( ta -> ( ch -> th ) ) )
8	7	a2d 23	. . . . . 6 |- ( y e. om -> ( ( ta -> ch ) -> ( ta -> th ) ) )
9		vex 2560	. . . . . . 7 |- y e. _V
10		finds2.2	. . . . . . . 8 |- ( x = y -> ( ph <-> ch ) )
11	10	imbi2d 219	. . . . . . 7 |- ( x = y -> ( ( ta -> ph ) <-> ( ta -> ch ) ) )
12	9, 11	elab 2687	. . . . . 6 |- ( y e. { x | ( ta -> ph ) } <-> ( ta -> ch ) )
13	9	sucex 4225	. . . . . . 7 |- suc y e. _V
14		finds2.3	. . . . . . . 8 |- ( x = suc y -> ( ph <-> th ) )
15	14	imbi2d 219	. . . . . . 7 |- ( x = suc y -> ( ( ta -> ph ) <-> ( ta -> th ) ) )
16	13, 15	elab 2687	. . . . . 6 |- ( suc y e. { x | ( ta -> ph ) } <-> ( ta -> th ) )
17	8, 12, 16	3imtr4g 194	. . . . 5 |- ( y e. om -> ( y e. { x | ( ta -> ph ) } -> suc y e. { x | ( ta -> ph ) } ) )
18	17	rgen 2374	. . . 4 |- A. y e. om ( y e. { x | ( ta -> ph ) } -> suc y e. { x | ( ta -> ph ) } )
19		peano5 4321	. . . 4 |- ( ( (/) e. { x | ( ta -> ph ) } /\ A. y e. om ( y e. { x | ( ta -> ph ) } -> suc y e. { x | ( ta -> ph ) } ) ) -> om C_ { x | ( ta -> ph ) } )
20	6, 18, 19	mp2an 402	. . 3 |- om C_ { x | ( ta -> ph ) }
21	20	sseli 2941	. 2 |- ( x e. om -> x e. { x | ( ta -> ph ) } )
22		abid 2028	. 2 |- ( x e. { x | ( ta -> ph ) } <-> ( ta -> ph ) )
23	21, 22	sylib 127	1 |- ( x e. om -> ( ta -> ph ) )

Syntax hints:   -> wi 4   <-> wb 98   = wceq 1243   e. wcel 1393   {cab 2026   A.wral 2306   C_ wss 2917   (/)c0 3224   suc csuc 4102   omcom 4313

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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-iinf 4311

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-uni 3581  df-int 3616  df-suc 4108  df-iom 4314

This theorem is referenced by:  finds1  4325  frecrdg  5992  freccl  5993  nnacl  6059  nnmcl  6060  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  nnsucsssuc  6071  nntri3or  6072  nnaordi  6081  nnaword  6084  nnmordi  6089  nnaordex  6100  prarloclem3  6595  frec2uzzd  9186  frec2uzuzd  9188  frec2uzrdg  9195