Metamath Proof Explorer

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 ⊢x=∅→φ↔ψ
tfinds3.2 ⊢x=y→φ↔χ
tfinds3.3 ⊢x=suc⁡y→φ↔θ
tfinds3.4 ⊢x=A→φ↔τ
tfinds3.5 ⊢η→ψ
tfinds3.6 ⊢y∈On→η→χ→θ
tfinds3.7 ⊢Lim⁡x→η→∀y∈xχ→φ
Assertion tfinds3 ⊢A∈On→η→τ

Proof

Step Hyp Ref Expression
1 tfinds3.1 ⊢x=∅→φ↔ψ
2 tfinds3.2 ⊢x=y→φ↔χ
3 tfinds3.3 ⊢x=suc⁡y→φ↔θ
4 tfinds3.4 ⊢x=A→φ↔τ
5 tfinds3.5 ⊢η→ψ
6 tfinds3.6 ⊢y∈On→η→χ→θ
7 tfinds3.7 ⊢Lim⁡x→η→∀y∈xχ→φ
8 1 imbi2d ⊢x=∅→η→φ↔η→ψ
9 2 imbi2d ⊢x=y→η→φ↔η→χ
10 3 imbi2d ⊢x=suc⁡y→η→φ↔η→θ
11 4 imbi2d ⊢x=A→η→φ↔η→τ
12 6 a2d ⊢y∈On→η→χ→η→θ
13 r19.21v ⊢∀y∈xη→χ↔η→∀y∈xχ
14 7 a2d ⊢Lim⁡x→η→∀y∈xχ→η→φ
15 13 14 biimtrid ⊢Lim⁡x→∀y∈xη→χ→η→φ
16 8 9 10 11 5 12 15 tfinds ⊢A∈On→η→τ