Metamath Proof Explorer

Theorem fpr2

Description: Law of well-founded recursion over a partial order, part two. Now we establish the value of F within A . (Contributed by Scott Fenton, 11-Sep-2023) (Proof shortened by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	fprr.1	$⊢ F = frecs (R, A, G)$
	Assertion	fpr2	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in A) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})$

Proof

Step	Hyp	Ref	Expression
1		fprr.1	$⊢ F = frecs (R, A, G)$
2	1	fpr1	$⊢ (R Fr A \land R Po A \land R Se A) \to F Fn A$
3	2	fndmd	$⊢ (R Fr A \land R Po A \land R Se A) \to dom F = A$
4	3	eleq2d	$⊢ (R Fr A \land R Po A \land R Se A) \to (X \in dom F \leftrightarrow X \in A)$
5	4	biimpar	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in A) \to X \in dom F$
6	1	fpr2a	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})$
7	5 6	syldan	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in A) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})$