This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- 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 ) )