Theorem tfinds3 7581

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 343	. 2 ⊢ (𝑥 = ∅ → ((𝜂 → 𝜑) ↔ (𝜂 → 𝜓)))
3		tfinds3.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
4	3	imbi2d 343	. 2 ⊢ (𝑥 = 𝑦 → ((𝜂 → 𝜑) ↔ (𝜂 → 𝜒)))
5		tfinds3.3	. . 3 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
6	5	imbi2d 343	. 2 ⊢ (𝑥 = suc 𝑦 → ((𝜂 → 𝜑) ↔ (𝜂 → 𝜃)))
7		tfinds3.4	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
8	7	imbi2d 343	. 2 ⊢ (𝑥 = 𝐴 → ((𝜂 → 𝜑) ↔ (𝜂 → 𝜏)))
9		tfinds3.5	. 2 ⊢ (𝜂 → 𝜓)
10		tfinds3.6	. . 3 ⊢ (𝑦 ∈ On → (𝜂 → (𝜒 → 𝜃)))
11	10	a2d 29	. 2 ⊢ (𝑦 ∈ On → ((𝜂 → 𝜒) → (𝜂 → 𝜃)))
12		r19.21v 3177	. . 3 ⊢ (∀𝑦 ∈ 𝑥 (𝜂 → 𝜒) ↔ (𝜂 → ∀𝑦 ∈ 𝑥 𝜒))
13		tfinds3.7	. . . 4 ⊢ (Lim 𝑥 → (𝜂 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))
14	13	a2d 29	. . 3 ⊢ (Lim 𝑥 → ((𝜂 → ∀𝑦 ∈ 𝑥 𝜒) → (𝜂 → 𝜑)))
15	12, 14	syl5bi 244	. 2 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝜂 → 𝜒) → (𝜂 → 𝜑)))
16	2, 4, 6, 8, 9, 11, 15	tfinds 7576	1 ⊢ (𝐴 ∈ On → (𝜂 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  ∀wral 3140  ∅c0 4293  Oncon0 6193  Lim wlim 6194  suc csuc 6195

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-tr 5175  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199

This theorem is referenced by:  oacl  8162  omcl  8163  oecl  8164  oawordri  8178  oaass  8189  oarec  8190  omordi  8194  omwordri  8200  odi  8207  omass  8208  oen0  8214  oewordri  8220  oeworde  8221  oeoelem  8226  omabs  8276  tfindsd  40571