wfr3

Description: The principle of Well-Ordered Recursion, part 3 of 3. 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 wfr1 and wfr2 is identical to F . (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	wfr3.3	$⊢ F = wrecs (R, A, G)$
	Assertion	wfr3	$⊢ ((R We A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)}))) \to F = H$

Proof

Step	Hyp	Ref	Expression
1		wfr3.3	$⊢ F = wrecs (R, A, G)$
2		simpl	$⊢ ((R We A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)}))) \to (R We A \land R Se A)$
3	1	wfr1	$⊢ (R We A \land R Se A) \to F Fn A$
4	1	wfr2	$⊢ ((R We A \land R Se A) \land z \in A) \to F (z) = G ({F ↾}_{Pred (R, A, z)})$
5	4	ralrimiva	$⊢ (R We A \land R Se A) \to \forall z \in A F (z) = G ({F ↾}_{Pred (R, A, z)})$
6	3 5	jca	$⊢ (R We A \land R Se A) \to (F Fn A \land \forall z \in A F (z) = G ({F ↾}_{Pred (R, A, z)}))$
7	6	adantr	$⊢ ((R We A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)}))) \to (F Fn A \land \forall z \in A F (z) = G ({F ↾}_{Pred (R, A, z)}))$
8		simpr	$⊢ ((R We A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)}))) \to (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)}))$
9		wfr3g	$⊢ ((R We A \land R Se A) \land (F Fn A \land \forall z \in A F (z) = G ({F ↾}_{Pred (R, A, z)})) \land (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)}))) \to F = H$
10	2 7 8 9	syl3anc	$⊢ ((R We A \land R Se A) \land (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)}))) \to F = H$

Metamath Proof Explorer

Theorem wfr3

Proof