Theorem finds1 4350

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, 22-Mar-2006.)

Hypotheses

Ref	Expression
finds1.1	⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
finds1.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
finds1.3	⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
finds1.4	⊢ 𝜓
finds1.5	⊢ (𝑦 ∈ ω → (𝜒 → 𝜃))

Assertion

Ref	Expression
finds1	⊢ (𝑥 ∈ ω → 𝜑)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)

Proof of Theorem finds1

Step	Hyp	Ref	Expression
1		eqid 2054	. 2 ⊢ ∅ = ∅
2		finds1.1	. . 3 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
3		finds1.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
4		finds1.3	. . 3 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
5		finds1.4	. . . 4 ⊢ 𝜓
6	5	a1i 9	. . 3 ⊢ (∅ = ∅ → 𝜓)
7		finds1.5	. . . 4 ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃))
8	7	a1d 22	. . 3 ⊢ (𝑦 ∈ ω → (∅ = ∅ → (𝜒 → 𝜃)))
9	2, 3, 4, 6, 8	finds2 4349	. 2 ⊢ (𝑥 ∈ ω → (∅ = ∅ → 𝜑))
10	1, 9	mpi 15	1 ⊢ (𝑥 ∈ ω → 𝜑)

Syntax hints:   → wi 4   ↔ wb 102   = wceq 1257   ∈ wcel 1407  ∅c0 3249  suc csuc 4127  ωcom 4338

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-13 1418  ax-14 1419  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-sep 3900  ax-nul 3908  ax-pow 3952  ax-pr 3969  ax-un 4195  ax-iinf 4336

This theorem depends on definitions:  df-bi 114  df-3an 896  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ral 2326  df-rex 2327  df-v 2574  df-dif 2945  df-un 2947  df-in 2949  df-ss 2956  df-nul 3250  df-pw 3386  df-sn 3406  df-pr 3407  df-uni 3606  df-int 3641  df-suc 4133  df-iom 4339

This theorem is referenced by:  findcard  6373  findcard2  6374  findcard2s  6375