Metamath Proof Explorer

Theorem fprfung

Description: A "function" defined by well-founded recursion is indeed a function when the relationship is a partial order. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	fprfung.1	$⊢ F = frecs (R, A, G)$
	Assertion	fprfung	$⊢ (R Fr A \land R Po A \land R Se A) \to Fun F$

Proof

Step	Hyp	Ref	Expression
1		fprfung.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	fprlem1	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in \{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)}))\} \land h \in \{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)}))\})) \to ((x g u \land x h v) \to u = v)$
4	2 1 3	frrlem9	$⊢ (R Fr A \land R Po A \land R Se A) \to Fun F$