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

Metamath Proof Explorer

Theorem frrrel

Description: Show without using the axiom of replacement that the well-founded recursion generator gives a relation. (Contributed by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	frrrel.1	$⊢ F = frecs (R, A, G)$
	Assertion	frrrel	$⊢ Rel F$

Proof

Step	Hyp	Ref	Expression
1		frrrel.1	$⊢ F = frecs (R, A, G)$
2		eqid	$⊢ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\} = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
3	2 1	frrlem6	$⊢ Rel F$