Metamath Proof Explorer


Theorem rtrclind

Description: Principle of transitive induction. The first three hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction step. (Contributed by Drahflow, 12-Nov-2015) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypotheses rtrclind.1 ηRelR
rtrclind.2 ηSV
rtrclind.3 ηXW
rtrclind.4 i=Sφχ
rtrclind.5 i=xφψ
rtrclind.6 i=jφθ
rtrclind.7 x=Xψτ
rtrclind.8 ηχ
rtrclind.9 ηjRxθψ
Assertion rtrclind ηSt*RXτ

Proof

Step Hyp Ref Expression
1 rtrclind.1 ηRelR
2 rtrclind.2 ηSV
3 rtrclind.3 ηXW
4 rtrclind.4 i=Sφχ
5 rtrclind.5 i=xφψ
6 rtrclind.6 i=jφθ
7 rtrclind.7 x=Xψτ
8 rtrclind.8 ηχ
9 rtrclind.9 ηjRxθψ
10 1 dfrtrcl2 ηt*R=t*recR
11 1 dfrtrclrec2 ηSt*recRXn0SRrnX
12 11 biimpac St*recRXηn0SRrnX
13 simprl St*recRXηSRrnXn0η
14 simprrr St*recRXηSRrnXn0n0
15 simprrl St*recRXηSRrnXn0SRrnX
16 1 2 3 4 5 6 7 8 9 relexpind ηn0SRrnXτ
17 13 14 15 16 syl3c St*recRXηSRrnXn0τ
18 17 anassrs St*recRXηSRrnXn0τ
19 18 expcom SRrnXn0St*recRXητ
20 19 expcom n0SRrnXSt*recRXητ
21 20 rexlimiv n0SRrnXSt*recRXητ
22 12 21 mpcom St*recRXητ
23 22 expcom ηSt*recRXτ
24 breq t*R=t*recRSt*RXSt*recRX
25 24 imbi1d t*R=t*recRSt*RXτSt*recRXτ
26 23 25 syl5ibr t*R=t*recRηSt*RXτ
27 10 26 mpcom ηSt*RXτ