Theorem findes

Description: Finite induction with explicit substitution. The first hypothesis is the basis and the second is the induction step. Theorem Schema 22 of Suppes p. 136. See tfindes for the transfinite version. This is an alternative for Metamath 100 proof #74. (Contributed by Raph Levien, 9-Jul-2003)

	Ref	Expression
Hypotheses	findes.1	|- [. (/) / x ]. ph
	findes.2	|- ( x e. _om -> ( ph -> [. suc x / x ]. ph ) )
Assertion	findes	|- ( x e. _om -> ph )

Proof

Step	Hyp	Ref	Expression
1		findes.1	|- [. (/) / x ]. ph
2		findes.2	|- ( x e. _om -> ( ph -> [. suc x / x ]. ph ) )
3		dfsbcq2	|- ( z = (/) -> ( [ z / x ] ph <-> [. (/) / x ]. ph ) )
4		sbequ	|- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
5		dfsbcq2	|- ( z = suc y -> ( [ z / x ] ph <-> [. suc y / x ]. ph ) )
6		sbequ12r	|- ( z = x -> ( [ z / x ] ph <-> ph ) )
7		nfv	|- F/ x y e. _om
8		nfs1v	|- F/ x [ y / x ] ph
9		nfsbc1v	|- F/ x [. suc y / x ]. ph
10	8 9	nfim	|- F/ x ( [ y / x ] ph -> [. suc y / x ]. ph )
11	7 10	nfim	|- F/ x ( y e. _om -> ( [ y / x ] ph -> [. suc y / x ]. ph ) )
12		eleq1w	|- ( x = y -> ( x e. _om <-> y e. _om ) )
13		sbequ12	|- ( x = y -> ( ph <-> [ y / x ] ph ) )
14		suceq	|- ( x = y -> suc x = suc y )
15	14	sbceq1d	|- ( x = y -> ( [. suc x / x ]. ph <-> [. suc y / x ]. ph ) )
16	13 15	imbi12d	|- ( x = y -> ( ( ph -> [. suc x / x ]. ph ) <-> ( [ y / x ] ph -> [. suc y / x ]. ph ) ) )
17	12 16	imbi12d	|- ( x = y -> ( ( x e. _om -> ( ph -> [. suc x / x ]. ph ) ) <-> ( y e. _om -> ( [ y / x ] ph -> [. suc y / x ]. ph ) ) ) )
18	11 17 2	chvarfv	|- ( y e. _om -> ( [ y / x ] ph -> [. suc y / x ]. ph ) )
19	3 4 5 6 1 18	finds	|- ( x e. _om -> ph )