Theorem tfinds3 7758

Description: Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. (Contributed by NM, 6-Jan-2005.) (Revised by David Abernethy, 21-Jun-2011.)

Hypotheses

Ref	Expression
tfinds3.1	⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
tfinds3.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
tfinds3.3	⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
tfinds3.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
tfinds3.5	⊢ (𝜂 → 𝜓)
tfinds3.6	⊢ (𝑦 ∈ On → (𝜂 → (𝜒 → 𝜃)))
tfinds3.7	⊢ (Lim 𝑥 → (𝜂 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))

Assertion

Ref	Expression
tfinds3	⊢ (𝐴 ∈ On → (𝜂 → 𝜏))

Distinct variable groups:   𝑥,𝐴   𝜑,𝑦   𝜒,𝑥   𝜏,𝑥   𝑥,𝑦,𝜂

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

Proof of Theorem tfinds3

Step	Hyp	Ref	Expression
1		tfinds3.1	. . 3 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
2	1	imbi2d 340	. 2 ⊢ (𝑥 = ∅ → ((𝜂 → 𝜑) ↔ (𝜂 → 𝜓)))
3		tfinds3.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
4	3	imbi2d 340	. 2 ⊢ (𝑥 = 𝑦 → ((𝜂 → 𝜑) ↔ (𝜂 → 𝜒)))
5		tfinds3.3	. . 3 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
6	5	imbi2d 340	. 2 ⊢ (𝑥 = suc 𝑦 → ((𝜂 → 𝜑) ↔ (𝜂 → 𝜃)))
7		tfinds3.4	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
8	7	imbi2d 340	. 2 ⊢ (𝑥 = 𝐴 → ((𝜂 → 𝜑) ↔ (𝜂 → 𝜏)))
9		tfinds3.5	. 2 ⊢ (𝜂 → 𝜓)
10		tfinds3.6	. . 3 ⊢ (𝑦 ∈ On → (𝜂 → (𝜒 → 𝜃)))
11	10	a2d 29	. 2 ⊢ (𝑦 ∈ On → ((𝜂 → 𝜒) → (𝜂 → 𝜃)))
12		r19.21v 3173	. . 3 ⊢ (∀𝑦 ∈ 𝑥 (𝜂 → 𝜒) ↔ (𝜂 → ∀𝑦 ∈ 𝑥 𝜒))
13		tfinds3.7	. . . 4 ⊢ (Lim 𝑥 → (𝜂 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
14	13	a2d 29	. . 3 ⊢ (Lim 𝑥 → ((𝜂 → ∀𝑦 ∈ 𝑥 𝜒) → (𝜂 → 𝜑)))
15	12, 14	biimtrid 241	. 2 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜂 → 𝜒) → (𝜂 → 𝜑)))
16	2, 4, 6, 8, 9, 11, 15	tfinds 7753	1 ⊢ (𝐴 ∈ On → (𝜂 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  ∀wral 3062  ∅c0 4267  Oncon0 6289  Lim wlim 6290  suc csuc 6291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7630

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-tr 5205  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295

This theorem is referenced by:  oacl  8415  omcl  8416  oecl  8417  oawordri  8431  oaass  8442  oarec  8443  omordi  8447  omwordri  8453  odi  8460  omass  8461  oen0  8467  oewordri  8473  oeworde  8474  oeoelem  8479  omabs  8531  tfindsd  42057