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

Metamath Proof Explorer

Theorem wfrdmcl

Description: The predecessor class of an element of the well-ordered recursion generator's domain is a subset of its domain. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011) (Proof shortened by Scott Fenton, 17-Nov-2024)

		Ref	Expression
	Hypothesis	wfrrel.1	$⊢ F = wrecs (R, A, G)$
	Assertion	wfrdmcl	$⊢ X \in dom F \to Pred (R, A, X) \subseteq dom F$

Proof

Step	Hyp	Ref	Expression
1		wfrrel.1	$⊢ F = wrecs (R, A, G)$
2		df-wrecs	$⊢ wrecs (R, A, G) = frecs (R, A, G \circ 2^{nd})$
3	1 2	eqtri	$⊢ F = frecs (R, A, G \circ 2^{nd})$
4	3	frrdmcl	$⊢ X \in dom F \to Pred (R, A, X) \subseteq dom F$