Theorem finds 7919

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 5313	. . . . . 6 ⊢ ∅ ∈ V
3		finds.1	. . . . . 6 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
4	2, 3	elab 3681	. . . . 5 ⊢ (∅ ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
5	1, 4	mpbir 231	. . . 4 ⊢ ∅ ∈ {𝑥 ∣ 𝜑}
6		finds.6	. . . . . 6 ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃))
7		vex 3482	. . . . . . 7 ⊢ 𝑦 ∈ V
8		finds.2	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
9	7, 8	elab 3681	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)
10	7	sucex 7826	. . . . . . 7 ⊢ suc 𝑦 ∈ V
11		finds.3	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
12	10, 11	elab 3681	. . . . . 6 ⊢ (suc 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜃)
13	6, 9, 12	3imtr4g 296	. . . . 5 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑}))
14	13	rgen 3061	. . . 4 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})
15		peano5 7916	. . . 4 ⊢ ((∅ ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) → ω ⊆ {𝑥 ∣ 𝜑})
16	5, 14, 15	mp2an 692	. . 3 ⊢ ω ⊆ {𝑥 ∣ 𝜑}
17	16	sseli 3991	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ {𝑥 ∣ 𝜑})
18		finds.4	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
19	18	elabg 3677	. 2 ⊢ (𝐴 ∈ ω → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜏))
20	17, 19	mpbid 232	1 ⊢ (𝐴 ∈ ω → 𝜏)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {cab 2712  ∀wral 3059   ⊆ wss 3963  ∅c0 4339  suc csuc 6388  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-om 7888

This theorem is referenced by:  findsg  7920  findes  7923  seqomlem1  8489  nna0r  8646  nnm0r  8647  nnawordi  8658  nneob  8693  naddoa  8739  enrefnn  9086  pssnn  9207  nneneq  9244  nneneqOLD  9256  inf3lem1  9666  inf3lem2  9667  cantnfval2  9707  cantnfp1lem3  9718  ttrclss  9758  ttrclselem2  9764  r1fin  9811  ackbij1lem14  10270  ackbij1lem16  10272  ackbij1  10275  ackbij2lem2  10277  ackbij2lem3  10278  infpssrlem4  10344  fin23lem14  10371  fin23lem34  10384  itunitc1  10458  ituniiun  10460  om2uzuzi  13987  om2uzlti  13988  om2uzrdg  13994  uzrdgxfr  14005  hashgadd  14413  mreexexd  17693  precsexlem8  28253  precsexlem9  28254  om2noseqrdg  28325  dfnns2  28377  constrfin  33751  satfrel  35352  satfdm  35354  satfrnmapom  35355  satf0op  35362  satf0n0  35363  sat1el2xp  35364  fmlafvel  35370  fmlaomn0  35375  gonar  35380  goalr  35382  satffun  35394  findfvcl  36435  finxp00  37385  onmcl  43321  naddonnn  43385