Theorem finds 7838

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.)

Hypotheses

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

Assertion

Ref	Expression
finds	⊢ (𝐴 ∈ ω → 𝜏)

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

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

Proof of Theorem finds

Step	Hyp	Ref	Expression
1		finds.5	. . . . 5 ⊢ 𝜓
2		0ex 5242	. . . . . 6 ⊢ ∅ ∈ V
3		finds.1	. . . . . 6 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
4	2, 3	elab 3623	. . . . 5 ⊢ (∅ ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
5	1, 4	mpbir 231	. . . 4 ⊢ ∅ ∈ {𝑥 ∣ 𝜑}
6		finds.6	. . . . . 6 ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃))
7		vex 3434	. . . . . . 7 ⊢ 𝑦 ∈ V
8		finds.2	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
9	7, 8	elab 3623	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)
10	7	sucex 7751	. . . . . . 7 ⊢ suc 𝑦 ∈ V
11		finds.3	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
12	10, 11	elab 3623	. . . . . 6 ⊢ (suc 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜃)
13	6, 9, 12	3imtr4g 296	. . . . 5 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑}))
14	13	rgen 3054	. . . 4 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})
15		peano5 7835	. . . 4 ⊢ ((∅ ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) → ω ⊆ {𝑥 ∣ 𝜑})
16	5, 14, 15	mp2an 693	. . 3 ⊢ ω ⊆ {𝑥 ∣ 𝜑}
17	16	sseli 3918	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ {𝑥 ∣ 𝜑})
18		finds.4	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
19	18	elabg 3620	. 2 ⊢ (𝐴 ∈ ω → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜏))
20	17, 19	mpbid 232	1 ⊢ (𝐴 ∈ ω → 𝜏)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052   ⊆ wss 3890  ∅c0 4274  suc csuc 6317  ωcom 7808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-om 7809

This theorem is referenced by:  findsg  7839  findes  7842  seqomlem1  8380  nna0r  8536  nnm0r  8537  nnawordi  8548  nneob  8583  naddoa  8629  enrefnn  8984  pssnn  9094  nneneq  9131  inf3lem1  9538  inf3lem2  9539  cantnfval2  9579  cantnfp1lem3  9590  ttrclss  9630  ttrclselem2  9636  r1fin  9686  ackbij1lem14  10143  ackbij1lem16  10145  ackbij1  10148  ackbij2lem2  10150  ackbij2lem3  10151  infpssrlem4  10217  fin23lem14  10244  fin23lem34  10257  itunitc1  10331  ituniiun  10333  om2uzuzi  13900  om2uzlti  13901  om2uzrdg  13907  uzrdgxfr  13918  hashgadd  14328  mreexexd  17603  precsexlem8  28225  precsexlem9  28226  om2noseqrdg  28315  bdayn0sf1o  28381  dfnns2  28383  constrfin  33911  constrextdg2  33914  satfrel  35570  satfdm  35572  satfrnmapom  35573  satf0op  35580  satf0n0  35581  sat1el2xp  35582  fmlafvel  35588  fmlaomn0  35593  gonar  35598  goalr  35600  satffun  35612  findfvcl  36655  finxp00  37729  onmcl  43774  naddonnn  43838