This theorem states that the solution to a well-founded recursion must be unique.
Proof sketch
Let f, g be two solutions of the recurrence. We want to show f = g.
By function extensionality it suffices to show ∀x ∈ X. f x = g x.
Induction over x. The induction hypothesis has the
equivalent transformation
∀u ∈ X. (u, x) ∈ R → f u = g u
↔ ∀u ∈ R⁻¹ {x}. f u = g u
↔ f|R⁻¹ {x} = g|R⁻¹ {x}.
We need to show f x = g x. Now, by the given recurrences we obtain
f x = φ x (f|R⁻¹ {x}) = φ x (g|R⁻¹ {x}) = g x. q.e.d.
Proof
01. 1 ⊢ wf R X, hypo.
02. 2 ⊢ ∀u. u ∈ X → (u, x) ∈ R → app f u = app g u, hypo.
03. 2 ⊢ u ∈ X → (u, x) ∈ R → app f u = app g u, uq_elim 2.
04. 4 ⊢ u ∈ inv_img R {x}, hypo.
05. 4 ⊢ ∃y. y ∈ {x} ∧ (u, y) ∈ R, inv_img_elim 4.
06. 6 ⊢ y ∈ {x} ∧ (u, y) ∈ R, hypo.
07. 6 ⊢ y ∈ {x}, conj_eliml 6.
08. 8 ⊢ x ∈ X, hypo.
09. 8 ⊢ set x, set_intro 8.
10. 8, 6 ⊢ y = x, sg_elim 9 7.
11. 6 ⊢ (u, y) ∈ R, conj_elimr 6.
12. 8, 6 ⊢ (u, x) ∈ R, eq_subst 10 11, P x ↔ (u, x) ∈ R.
13. 8, 4 ⊢ (u, x) ∈ R, ex_elim 5 12.
14. 14 ⊢ dom R ⊆ X, hypo.
15. 8, 4 ⊢ u ∈ dom R, dom_intro 13.
16. 14, 8, 4 ⊢ u ∈ X, incl_elim 14 15.
17. 14, 2, 8, 4 ⊢ (u, x) ∈ R → app f u = app g u, subj_elim 3 16.
18. 14, 2, 8, 4 ⊢ app f u = app g u, subj_elim 17 13.
19. 19 ⊢ map f X Y, hypo.
20. 20 ⊢ map g X Y, hypo.
21. ⊢ inv_img R {x} ⊆ dom R, inv_img_incl_in_dom.
22. 14 ⊢ inv_img R {x} ⊆ X, incl_trans 21 14.
23. 19, 14, 4 ⊢ app f u = app (restr f (inv_img R {x})) u, app_restr 19 22 4.
24. 20, 14, 4 ⊢ app g u = app (restr g (inv_img R {x})) u, app_restr 20 22 4.
25. 19, 14, 2, 8, 4 ⊢ app (restr f (inv_img R {x})) u = app g u,
eq_subst 23 18, P t ↔ t = app g u.
26. 19, 20, 14, 2, 8, 4 ⊢
app (restr f (inv_img R {x})) u = app (restr g (inv_img R {x})) u,
eq_subst 24 25, P t ↔ app (restr f (inv_img R {x})) u = t.
27. 19, 20, 14, 2, 8 ⊢ u ∈ inv_img R {x} →
app (restr f (inv_img R {x})) u = app (restr g (inv_img R {x})) u,
subj_intro 26.
28. 19, 20, 14, 2, 8 ⊢ ∀u. u ∈ inv_img R {x} →
app (restr f (inv_img R {x})) u = app (restr g (inv_img R {x})) u,
uq_intro 27.
29. 19, 14 ⊢ map (restr f (inv_img R {x})) (inv_img R {x}) Y, map_restr 19 22.
30. 20, 14 ⊢ map (restr g (inv_img R {x})) (inv_img R {x}) Y, map_restr 20 22.
31. 19, 20, 14, 2, 8 ⊢ restr f (inv_img R {x}) = restr g (inv_img R {x}),
map_extensionality 29 30 28.
32. 32 ⊢ ∀x. x ∈ X → app f x = φ x (restr f (inv_img R {x})), hypo.
33. 33 ⊢ ∀x. x ∈ X → app g x = φ x (restr g (inv_img R {x})), hypo.
34. 32 ⊢ x ∈ X → app f x = φ x (restr f (inv_img R {x})), uq_elim 32.
35. 33 ⊢ x ∈ X → app g x = φ x (restr g (inv_img R {x})), uq_elim 33.
36. 32, 8 ⊢ app f x = φ x (restr f (inv_img R {x})), subj_elim 34 8.
37. 33, 8 ⊢ app g x = φ x (restr g (inv_img R {x})), subj_elim 35 8.
38. 19, 20, 14, 32, 2, 8 ⊢ app f x = φ x (restr g (inv_img R {x})),
eq_subst 31 36, P t ↔ app f x = φ x t.
39. 19, 20, 14, 32, 33, 8, 2 ⊢ app f x = app g x,
eq_subst_rev 37 38, P t ↔ app f x = t.
40. 19, 20, 14, 32, 33, 8 ⊢
(∀u. u ∈ X → (u, x) ∈ R → app f u = app g u) →
app f x = app g x, subj_intro 39.
41. 19, 20, 14, 32, 33 ⊢
x ∈ X → (∀u. u ∈ X → (u, x) ∈ R → app f u = app g u) →
app f x = app g x, subj_intro 40.
42. 19, 20, 14, 32, 33 ⊢
∀x. x ∈ X → (∀u. u ∈ X → (u, x) ∈ R → app f u = app g u) →
app f x = app g x, uq_intro 41.
43. 1, 19, 20, 14, 32, 33 ⊢
∀x. x ∈ X → app f x = app g x, wf_induction 1 42.
44. 1, 14, 19, 20, 32, 33 ⊢ f = g, map_extensionality 19 20 43.
45. 1, 14, 19, 20 ⊢
(∀x. x ∈ X → app f x = φ x (restr f (inv_img R {x}))) →
(∀x. x ∈ X → app g x = φ x (restr g (inv_img R {x}))) →
f = g, subj_intro_ii 44.
wf_rec_unique. ⊢ wf R X → dom R ⊆ X → map f X Y → map g X Y →
(∀x. x ∈ X → app f x = φ x (restr f (inv_img R {x}))) →
(∀x. x ∈ X → app g x = φ x (restr g (inv_img R {x}))) →
f = g, subj_intro_iv 45.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.