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	|- A e. _V
Assertion	tz9.12	|- ( A. x e. A E. y e. On x e. ( R1 ` y ) -> E. y e. On A e. ( R1 ` y ) )

Proof

Step	Hyp	Ref	Expression
1		tz9.12.1	|- A e. _V
2		eqid	|- ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) = ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } )
3	1 2	tz9.12lem2	|- suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) e. On
4	3	onsuci	|- suc suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) e. On
5	1 2	tz9.12lem3	|- ( A. x e. A E. y e. On x e. ( R1 ` y ) -> A e. ( R1 ` suc suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) ) )
6		fveq2	|- ( y = suc suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) -> ( R1 ` y ) = ( R1 ` suc suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) ) )
7	6	eleq2d	|- ( y = suc suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) -> ( A e. ( R1 ` y ) <-> A e. ( R1 ` suc suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) ) ) )
8	7	rspcev	|- ( ( suc suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) e. On /\ A e. ( R1 ` suc suc U. ( ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } ) " A ) ) ) -> E. y e. On A e. ( R1 ` y ) )
9	4 5 8	sylancr	|- ( A. x e. A E. y e. On x e. ( R1 ` y ) -> E. y e. On A e. ( R1 ` y ) )