This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ [ ∅ / 𝑥 ] 𝜑
findes.2 ⊢ ( 𝑥 ∈ ω → ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) )
Assertion findes ( 𝑥 ∈ ω → 𝜑 )

Proof

Step Hyp Ref Expression
1 findes.1 ⊢ [ ∅ / 𝑥 ] 𝜑
2 findes.2 ⊢ ( 𝑥 ∈ ω → ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) )
3 dfsbcq2 ⊢ ( 𝑧 = ∅ → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ ∅ / 𝑥 ] 𝜑 ) )
4 sbequ ⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
5 dfsbcq2 ⊢ ( 𝑧 = suc 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ suc 𝑦 / 𝑥 ] 𝜑 ) )
6 sbequ12r ⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
7 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ ω
8 nfs1v ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
9 nfsbc1v ⊢ Ⅎ 𝑥 [ suc 𝑦 / 𝑥 ] 𝜑
10 8 9 nfim ⊢ Ⅎ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 )
11 7 10 nfim ⊢ Ⅎ 𝑥 ( 𝑦 ∈ ω → ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) )
12 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ω ↔ 𝑦 ∈ ω ) )
13 sbequ12 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
14 suceq ⊢ ( 𝑥 = 𝑦 → suc 𝑥 = suc 𝑦 )
15 14 sbceq1d ⊢ ( 𝑥 = 𝑦 → ( [ suc 𝑥 / 𝑥 ] 𝜑 ↔ [ suc 𝑦 / 𝑥 ] 𝜑 ) )
16 13 15 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) ) )
17 12 16 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ω → ( 𝜑 → [ suc 𝑥 / 𝑥 ] 𝜑 ) ) ↔ ( 𝑦 ∈ ω → ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) ) ) )
18 11 17 2 chvarfv ⊢ ( 𝑦 ∈ ω → ( [ 𝑦 / 𝑥 ] 𝜑 → [ suc 𝑦 / 𝑥 ] 𝜑 ) )
19 3 4 5 6 1 18 finds ⊢ ( 𝑥 ∈ ω → 𝜑 )