Metamath Proof Explorer


Theorem finds

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)

Ref Expression
Hypotheses finds.1 x=φψ
finds.2 x=yφχ
finds.3 x=sucyφθ
finds.4 x=Aφτ
finds.5 ψ
finds.6 yωχθ
Assertion finds Aωτ

Proof

Step Hyp Ref Expression
1 finds.1 x=φψ
2 finds.2 x=yφχ
3 finds.3 x=sucyφθ
4 finds.4 x=Aφτ
5 finds.5 ψ
6 finds.6 yωχθ
7 0ex V
8 7 1 elab x|φψ
9 5 8 mpbir x|φ
10 vex yV
11 10 2 elab yx|φχ
12 10 sucex sucyV
13 12 3 elab sucyx|φθ
14 6 11 13 3imtr4g yωyx|φsucyx|φ
15 14 rgen yωyx|φsucyx|φ
16 peano5 x|φyωyx|φsucyx|φωx|φ
17 9 15 16 mp2an ωx|φ
18 17 sseli AωAx|φ
19 4 elabg AωAx|φτ
20 18 19 mpbid Aωτ