Metamath Proof Explorer


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