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

Metamath Proof Explorer

Theorem wfrdmss

Description: The domain of the well-ordered recursion generator is a subclass of A . 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	wfrdmss	$⊢ dom F \subseteq A$

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	frrdmss	$⊢ dom F \subseteq A$