Theorem finds1 7612

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 2759	. 2 ⊢ ∅ = ∅
2		finds1.1	. . 3 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
3		finds1.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
4		finds1.3	. . 3 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
5		finds1.4	. . . 4 ⊢ 𝜓
6	5	a1i 11	. . 3 ⊢ (∅ = ∅ → 𝜓)
7		finds1.5	. . . 4 ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃))
8	7	a1d 25	. . 3 ⊢ (𝑦 ∈ ω → (∅ = ∅ → (𝜒 → 𝜃)))
9	2, 3, 4, 6, 8	finds2 7611	. 2 ⊢ (𝑥 ∈ ω → (∅ = ∅ → 𝜑))
10	1, 9	mpi 20	1 ⊢ (𝑥 ∈ ω → 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1539   ∈ wcel 2112  ∅c0 4226  suc csuc 6172  ωcom 7580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299  ax-un 7460

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-tr 5140  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-om 7581

This theorem is referenced by:  findcard  8782  findcard2  8783  findcard2OLD  8784  pwfi  8845  alephfplem3  9559  pwsdompw  9657  hsmexlem4  9882