Theorem tfinds3

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)

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

Proof

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