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

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