Metamath Proof Explorer

Theorem finds2

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 step. Theorem Schema 22 of Suppes p. 136. (Contributed by NM, 29-Nov-2002)

Ref Expression
Hypotheses finds2.1 ⊢ x = ∅ → φ ↔ ψ
finds2.2 ⊢ x = y → φ ↔ χ
finds2.3 ⊢ x = suc ⁡ y → φ ↔ θ
finds2.4 ⊢ τ → ψ
finds2.5 ⊢ y ∈ ω → τ → χ → θ
Assertion finds2 ⊢ x ∈ ω → τ → φ

Proof

Step Hyp Ref Expression
1 finds2.1 ⊢ x = ∅ → φ ↔ ψ
2 finds2.2 ⊢ x = y → φ ↔ χ
3 finds2.3 ⊢ x = suc ⁡ y → φ ↔ θ
4 finds2.4 ⊢ τ → ψ
5 finds2.5 ⊢ y ∈ ω → τ → χ → θ
6 0ex ⊢ ∅ ∈ V
7 1 imbi2d ⊢ x = ∅ → τ → φ ↔ τ → ψ
8 6 7 elab ⊢ ∅ ∈ x | τ → φ ↔ τ → ψ
9 4 8 mpbir ⊢ ∅ ∈ x | τ → φ
10 5 a2d ⊢ y ∈ ω → τ → χ → τ → θ
11 vex ⊢ y ∈ V
12 2 imbi2d ⊢ x = y → τ → φ ↔ τ → χ
13 11 12 elab ⊢ y ∈ x | τ → φ ↔ τ → χ
14 11 sucex ⊢ suc ⁡ y ∈ V
15 3 imbi2d ⊢ x = suc ⁡ y → τ → φ ↔ τ → θ
16 14 15 elab ⊢ suc ⁡ y ∈ x | τ → φ ↔ τ → θ
17 10 13 16 3imtr4g ⊢ y ∈ ω → y ∈ x | τ → φ → suc ⁡ y ∈ x | τ → φ
18 17 rgen ⊢ ∀ y ∈ ω y ∈ x | τ → φ → suc ⁡ y ∈ x | τ → φ
19 peano5 ⊢ ∅ ∈ x | τ → φ ∧ ∀ y ∈ ω y ∈ x | τ → φ → suc ⁡ y ∈ x | τ → φ → ω ⊆ x | τ → φ
20 9 18 19 mp2an ⊢ ω ⊆ x | τ → φ
21 20 sseli ⊢ x ∈ ω → x ∈ x | τ → φ
22 abid ⊢ x ∈ x | τ → φ ↔ τ → φ
23 21 22 sylib ⊢ x ∈ ω → τ → φ