fpr3

Description: Law of well-founded recursion over a partial order, part three. Finally, we show that F is unique. We do this by showing that any function H with the same properties we proved of F in fpr1 and fpr2 is identical to F . (Contributed by Scott Fenton, 11-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		fprr.1	$⊢ F = frecs (R, A, G)$
2		simpl	$⊢ ((R Fr A \land R Po A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = z G ({H ↾}_{Pred (R, A, z)}))) \to (R Fr A \land R Po A \land R Se A)$
3	1	fpr1	$⊢ (R Fr A \land R Po A \land R Se A) \to F Fn A$
4	1	fpr2	$⊢ ((R Fr A \land R Po A \land R Se A) \land z \in A) \to F (z) = z G ({F ↾}_{Pred (R, A, z)})$
5	4	ralrimiva	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall z \in A F (z) = z G ({F ↾}_{Pred (R, A, z)})$
6	3 5	jca	$⊢ (R Fr A \land R Po A \land R Se A) \to (F Fn A \land \forall z \in A F (z) = z G ({F ↾}_{Pred (R, A, z)}))$
7	6	adantr	$⊢ ((R Fr A \land R Po A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = z G ({H ↾}_{Pred (R, A, z)}))) \to (F Fn A \land \forall z \in A F (z) = z G ({F ↾}_{Pred (R, A, z)}))$
8		simpr	$⊢ ((R Fr A \land R Po A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = z G ({H ↾}_{Pred (R, A, z)}))) \to (H Fn A \land \forall z \in A H (z) = z G ({H ↾}_{Pred (R, A, z)}))$
9		fpr3g	$⊢ ((R Fr A \land R Po A \land R Se A) \land (F Fn A \land \forall z \in A F (z) = z G ({F ↾}_{Pred (R, A, z)})) \land (H Fn A \land \forall z \in A H (z) = z G ({H ↾}_{Pred (R, A, z)}))) \to F = H$
10	2 7 8 9	syl3anc	$⊢ ((R Fr A \land R Po A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = z G ({H ↾}_{Pred (R, A, z)}))) \to F = H$

Metamath Proof Explorer

Theorem fpr3

Proof