Theorem rankwflem

Description: Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of TakeutiZaring p. 78. This variant of tz9.13g is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003)

	Ref	Expression
Assertion	rankwflem	|- ( A e. V -> E. x e. On A e. ( R1 ` suc x ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. V -> A e. _V )
2		unir1	|- U. ( R1 " On ) = _V
3	1 2	eleqtrrdi	|- ( A e. V -> A e. U. ( R1 " On ) )
4		rankwflemb	|- ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )
5	3 4	sylib	|- ( A e. V -> E. x e. On A e. ( R1 ` suc x ) )