fn_on_extensionality

Theorem fn_on_extensionality

Theorem. fn_on_extensionality
fn_on f A → fn_on g A → (∀x. x ∈ A → app f x = app g x) → restr f A = restr g A

Proof
01. 1 ⊢ fn_on f A, hypo.
02. 2 ⊢ fn_on g A, hypo.
03. 3 ⊢ ∀x. x ∈ A → app f x = app g x, hypo.
04. 4 ⊢ t ∈ restr f A, hypo.
05. 4 ⊢ t ∈ f ∩ (A × UnivCl), eq_subst restr_eq 4, P u ↔ t ∈ u.
06. 4 ⊢ t ∈ f, intersection_eliml 5.
07. 4 ⊢ t ∈ A × UnivCl, intersection_elimr 5.
08. 1 ⊢ relation f, relation_from_fn_on 1.
09. 1 ⊢ ∀t. t ∈ f → ∃x. ∃y. t = (x, y), relation_unfold 8.
10. 1, 4 ⊢ ∃x. ∃y. t = (x, y), uq_bounded_elim 9 6.
11. 11 ⊢ ∃y. t = (x, y), hypo.
12. 12 ⊢ t = (x, y), hypo.
13. 4, 12 ⊢ (x, y) ∈ A × UnivCl, eq_subst 12 7.
14. 4, 12 ⊢ x ∈ A ∧ y ∈ UnivCl, prod_elim_pair 13.
15. 4, 12 ⊢ x ∈ A, conj_eliml 14.
16. 4, 12 ⊢ y ∈ UnivCl, conj_elimr 14.
17. 4, 12 ⊢ (x, y) ∈ f, eq_subst 12 6.
18. 1, 4, 12 ⊢ y = app f x, fn_on_app_intro 1 15 17.
19. 3, 4, 12 ⊢ app f x = app g x, uq_bounded_elim 3 15.
20. 1, 3, 4, 12 ⊢ y = app g x, eq_subst 19 18, P u ↔ y = u.
21. 1, 2, 3, 4, 12 ⊢ (x, y) ∈ g, fn_on_app_elim 2 15 20.
22. 1, 2, 3, 4, 12 ⊢ (x, y) ∈ g ∩ (A × UnivCl), intersection_intro 21 13.
23. ⊢ restr g A = g ∩ (A × UnivCl), restr_eq.
24. 1, 2, 3, 4, 12 ⊢ (x, y) ∈ restr g A, eq_subst_rev 23 22, P u ↔ (x, y) ∈ u.
25. 1, 2, 3, 4, 12 ⊢ t ∈ restr g A, eq_subst_rev 12 24, P u ↔ u ∈ restr g A.
26. 1, 2, 3, 4, 11 ⊢ t ∈ restr g A, ex_elim 11 25.
27. 1, 2, 3, 4 ⊢ t ∈ restr g A, ex_elim 10 26.
28. 1, 2, 3 ⊢ t ∈ restr f A → t ∈ restr g A, subj_intro 27.
29. 1, 2, 3 ⊢ ∀t. t ∈ restr f A → t ∈ restr g A, uq_intro 28.
30. 1, 2, 3 ⊢ restr f A ⊆ restr g A, incl_intro 29.
31. ⊢ fn_on f A → fn_on g A →
  (∀x. x ∈ A → app f x = app g x) →
  restr f A ⊆ restr g A, subj_intro_iii 30.
32. 32 ⊢ x ∈ A, hypo.
33. 3, 32 ⊢ app f x = app g x, uq_bounded_elim 3 32.
34. 3, 32 ⊢ app g x = app f x, eq_symm 33.
35. 3 ⊢ x ∈ A → app g x = app f x, subj_intro 34.
36. 3 ⊢ ∀x. x ∈ A → app g x = app f x, uq_intro 35.
37. 1, 2, 3 ⊢ restr g A ⊆ restr f A, 31 2 1 36.
38. 1, 2, 3 ⊢ restr f A = restr g A, incl_antisym 30 37.
fn_on_extensionality. ⊢ fn_on f A → fn_on g A →
  (∀x. x ∈ A → app f x = app g x) →
  restr f A = restr g A, subj_intro_iii 38.

Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.