Theorem finds2 7854

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, 29-Nov-2002.)

Hypotheses

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

Assertion

Ref	Expression
finds2	⊢ (𝑥 ∈ ω → (𝜏 → 𝜑))

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

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

Proof of Theorem finds2

Step	Hyp	Ref	Expression
1		finds2.4	. . . . 5 ⊢ (𝜏 → 𝜓)
2		0ex 5257	. . . . . 6 ⊢ ∅ ∈ V
3		finds2.1	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
4	3	imbi2d 340	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜓)))
5	2, 4	elab 3643	. . . . 5 ⊢ (∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜓))
6	1, 5	mpbir 231	. . . 4 ⊢ ∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)}
7		finds2.5	. . . . . . 7 ⊢ (𝑦 ∈ ω → (𝜏 → (𝜒 → 𝜃)))
8	7	a2d 29	. . . . . 6 ⊢ (𝑦 ∈ ω → ((𝜏 → 𝜒) → (𝜏 → 𝜃)))
9		vex 3448	. . . . . . 7 ⊢ 𝑦 ∈ V
10		finds2.2	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
11	10	imbi2d 340	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜒)))
12	9, 11	elab 3643	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜒))
13	9	sucex 7762	. . . . . . 7 ⊢ suc 𝑦 ∈ V
14		finds2.3	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
15	14	imbi2d 340	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜃)))
16	13, 15	elab 3643	. . . . . 6 ⊢ (suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜃))
17	8, 12, 16	3imtr4g 296	. . . . 5 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)}))
18	17	rgen 3046	. . . 4 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)})
19		peano5 7849	. . . 4 ⊢ ((∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)})) → ω ⊆ {𝑥 ∣ (𝜏 → 𝜑)})
20	6, 18, 19	mp2an 692	. . 3 ⊢ ω ⊆ {𝑥 ∣ (𝜏 → 𝜑)}
21	20	sseli 3939	. 2 ⊢ (𝑥 ∈ ω → 𝑥 ∈ {𝑥 ∣ (𝜏 → 𝜑)})
22		abid 2711	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜑))
23	21, 22	sylib 218	1 ⊢ (𝑥 ∈ ω → (𝜏 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044   ⊆ wss 3911  ∅c0 4292  suc csuc 6322  ωcom 7822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-om 7823

This theorem is referenced by:  finds1  7855  onnseq  8290  nnacl  8552  nnmcl  8553  nnecl  8554  nnacom  8558  nnaass  8563  nndi  8564  nnmass  8565  nnmsucr  8566  nnmcom  8567  nnmordi  8572  omsmolem  8598  isinf  9183  isinfOLD  9184  unblem2  9216  fiint  9253  fiintOLD  9254  dffi3  9358  card2inf  9484  cantnfle  9600  cantnflt  9601  cantnflem1  9618  cnfcom  9629  trcl  9657  fseqenlem1  9953  nnadju  10127  infpssrlem3  10234  fin23lem26  10254  axdc3lem2  10380  axdc4lem  10384  axdclem2  10449  wunr1om  10648  wuncval2  10676  tskr1om  10696  grothomex  10758  peano5nni  12165  precsexlem6  28090  precsexlem7  28091  noseqind  28162  om2noseqlt  28169  neibastop2lem  36321  finxpreclem6  37357  domalom  37365  oaabsb  43256