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	$⊢ A \in V \to \exists x \in On A \in R_{1} (suc x)$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in V \to A \in V$
2		unir1	$⊢ ⋃ R_{1} [On] = V$
3	1 2	eleqtrrdi	$⊢ A \in V \to A \in ⋃ R_{1} [On]$
4		rankwflemb	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists x \in On A \in R_{1} (suc x)$
5	3 4	sylib	$⊢ A \in V \to \exists x \in On A \in R_{1} (suc x)$