Theorem finds2 3220

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

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

Proof of Theorem finds2

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

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:  finds1 3221  omsmolem 4340  unblem2 4628  fiint 4644  trcl 4731  alephfplem3 4987

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