Theorem finds 7899

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 5272	. . . . . 6 ⊢ ∅ ∈ V
3		finds.1	. . . . . 6 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
4	2, 3	elab 3640	. . . . 5 ⊢ (∅ ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
5	1, 4	mpbir 234	. . . 4 ⊢ ∅ ∈ {𝑥 ∣ 𝜑}
6		finds.6	. . . . . 6 ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃))
7		vex 3461	. . . . . . 7 ⊢ 𝑦 ∈ V
8		finds.2	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
9	7, 8	elab 3640	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)
10	7	sucex 7811	. . . . . . 7 ⊢ suc 𝑦 ∈ V
11		finds.3	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
12	10, 11	elab 3640	. . . . . 6 ⊢ (suc 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜃)
13	6, 9, 12	3imtr4g 299	. . . . 5 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑}))
14	13	rgen 3083	. . . 4 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})
15		peano5 7896	. . . 4 ⊢ ((∅ ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) → ω ⊆ {𝑥 ∣ 𝜑})
16	5, 14, 15	mp2an 705	. . 3 ⊢ ω ⊆ {𝑥 ∣ 𝜑}
17	16	sseli 3934	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ {𝑥 ∣ 𝜑})
18		finds.4	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
19	18	elabg 3637	. 2 ⊢ (𝐴 ∈ ω → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜏))
20	17, 19	mpbid 235	1 ⊢ (𝐴 ∈ ω → 𝜏)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {cab 2743  ∀wral 3081   ⊆ wss 3906  ∅c0 4286  suc csuc 6366  ωcom 7868

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-om 7869

This theorem is used by:  findsg  7900  findes  7903  seqomlem1  8443  nna0r  8601  nnm0r  8602  nnawordi  8613  nneob  8648  naddoa  8695  enrefnn  9050  pssnn  9160  nneneq  9197  inf3lem1  9604  inf3lem2  9605  cantnfval2  9645  cantnfp1lem3  9656  ttrclss  9696  ttrclselem2  9702  r1fin  9752  ackbij1lem14  10231  ackbij1lem16  10233  ackbij1  10236  ackbij2lem2  10238  ackbij2lem3  10239  infpssrlem4  10305  fin23lem14  10332  fin23lem34  10345  itunitc1  10419  ituniiun  10421  om2uzuzi  14003  om2uzlti  14004  om2uzrdg  14010  uzrdgxfr  14021  hashgadd  14431  mreexexd  17726  precsexlem8  28458  precsexlem9  28459  om2noseqrdg  28548  bdayn0sf1o  28614  dfnns2  28616  constrfin  34200  constrextdg2  34203  satfrel  35896  satfdm  35898  satfrnmapom  35899  satf0op  35906  satf0n0  35907  sat1el2xp  35908  fmlafvel  35914  fmlaomn0  35919  gonar  35924  goalr  35926  satffun  35938  findfvcl  37020  finxp00  38105  onmcl  44116  naddonnn  44180