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	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		unir1	⊢ ∪ ( 𝑅1 “ On ) = V
3	1 2	eleqtrrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
4		rankwflemb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
5	3 4	sylib	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )