Theorem finds 3218

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 hypothesis. Theorem Schema 22 of [Suppes] p. 136.

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

Proof of Theorem finds

Step	Hyp	Ref	Expression
1		finds.5	. . . . 5 |- ps
2		0ex 2762	. . . . . 6 |- (/) e. V
3		finds.1	. . . . . 6 |- (x = (/) -> (ph <-> ps))
4	2, 3	elab 1935	. . . . 5 |- ((/) e. {x | ph} <-> ps)
5	1, 4	mpbir 188	. . . 4 |- (/) e. {x | ph}
6		finds.6	. . . . . 6 |- (y e. om -> (ch -> th))
7		visset 1851	. . . . . . 7 |- y e. V
8		finds.2	. . . . . . 7 |- (x = y -> (ph <-> ch))
9	7, 8	elab 1935	. . . . . 6 |- (y e. {x | ph} <-> ch)
10	7	sucex 3105	. . . . . . 7 |- suc y e. V
11		finds.3	. . . . . . 7 |- (x = suc y -> (ph <-> th))
12	10, 11	elab 1935	. . . . . 6 |- (suc y e. {x | ph} <-> th)
13	6, 9, 12	3imtr4g 555	. . . . 5 |- (y e. om -> (y e. {x | ph} -> suc y e. {x | ph}))
14	13	rgen 1736	. . . 4 |- A.y e. om (y e. {x | ph} -> suc y e. {x | ph})
15		peano5 3215	. . . 4 |- (((/) e. {x | ph} /\ A.y e. om (y e. {x | ph} -> suc y e. {x | ph})) -> om (_ {x | ph})
16	5, 14, 15	mp2an 700	. . 3 |- om (_ {x | ph}
17	16	sseli 2109	. 2 |- (A e. om -> A e. {x | ph})
18		finds.4	. . 3 |- (x = A -> (ph <-> ta))
19	18	elabg 1937	. 2 |- (A e. om -> (A e. {x | ph} <-> ta))
20	17, 19	mpbid 193	1 |- (A e. om -> ta)

Syntax hints:   -> wi 3   <-> wb 144   = wceq 988   e. wcel 990  {cab 1499  A.wral 1683   (_ wss 2091  (/)c0 2324  suc csuc 3005  omcom 3192

This theorem is referenced by:  findsg 3219  findes 3222  nnacl 4313  nnmcl 4314  nnecl 4315  nnacom 4317  nnmsucr 4324  nnmcom 4325  nneob 4339  nneneq 4601  pssnn 4623  inf3lem1 4699  inf3lem2 4700  om2uzuzi 6589  om2uzlti 6590  findfvcl 10539

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-nul 2761  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 779  df-3an 780  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-if 2407  df-pw 2447  df-sn 2457  df-pr 2458  df-tp 2460  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-tr 2732  df-eprel 2886  df-po 2894  df-so 2904  df-fr 2972  df-we 2989  df-ord 3006  df-on 3007  df-lim 3008  df-suc 3009  df-om 3193

Copyright terms: Public domain