map_extensionality

Theorem map_extensionality

Theorem. map_extensionality
map f X Y → map g X Y → (∀x. x ∈ X → app f x = app g x) → f = g

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ map g X Y, hypo.
03. 3 ⊢ ∀x. x ∈ X → app f x = app g x, hypo.
04. 3 ⊢ x ∈ X → app f x = app g x, uq_elim 3.
05. 5 ⊢ x ∈ X, hypo.
06. 3, 5 ⊢ app f x = app g x, subj_elim 4 5.
07. 3, 5 ⊢ app g x = app f x, eq_symm 6.
08. 3 ⊢ x ∈ X → app g x = app f x, subj_intro 7.
09. 3 ⊢ ∀x. x ∈ X → app g x = app f x, uq_intro 8.
10. 1, 2, 3 ⊢ f ⊆ g, map_extensionality_lemma 1 2 3.
11. 1, 2, 3 ⊢ g ⊆ f, map_extensionality_lemma 2 1 9.
12. 1, 2, 3 ⊢ f = g, incl_antisym 10 11.
map_extensionality. ⊢ map f X Y → map g X Y →
  (∀x. x ∈ X → app f x = app g x) → f = g, subj_intro_iii 12.

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