Metamath Proof Explorer


Theorem tz9.12

Description: A set is well-founded if all of its elements are well-founded. Proposition 9.12 of TakeutiZaring p. 78. The main proof consists of tz9.12lem1 through tz9.12lem3 . (Contributed by NM, 22-Sep-2003)

Ref Expression
Hypothesis tz9.12.1 AV
Assertion tz9.12 xAyOnxR1yyOnAR1y

Proof

Step Hyp Ref Expression
1 tz9.12.1 AV
2 eqid zVvOn|zR1v=zVvOn|zR1v
3 1 2 tz9.12lem2 suczVvOn|zR1vAOn
4 3 onsuci sucsuczVvOn|zR1vAOn
5 1 2 tz9.12lem3 xAyOnxR1yAR1sucsuczVvOn|zR1vA
6 fveq2 y=sucsuczVvOn|zR1vAR1y=R1sucsuczVvOn|zR1vA
7 6 eleq2d y=sucsuczVvOn|zR1vAAR1yAR1sucsuczVvOn|zR1vA
8 7 rspcev sucsuczVvOn|zR1vAOnAR1sucsuczVvOn|zR1vAyOnAR1y
9 4 5 8 sylancr xAyOnxR1yyOnAR1y