Theorem composition_inj_inj_is_inj

Proof
01. 1 ⊢ inj f X Y, hypo.
02. 2 ⊢ inj g Y Z, hypo.
03. 1 ⊢ map f X Y, inj_is_map 1.
04. 2 ⊢ map g Y Z, inj_is_map 2.
05. 1, 2 ⊢ map (g ∘ f) X Z, composition_is_map 3 4.
06. 6 ⊢ a ∈ X, hypo.
07. 7 ⊢ b ∈ X, hypo.
08. 8 ⊢ app (g ∘ f) a = app (g ∘ f) b, hypo.
09. 1, 2, 6 ⊢ app (g ∘ f) a = app g (app f a),
  map_app_composition 3 4 6.
10. 1, 2, 7 ⊢ app (g ∘ f) b = app g (app f b),
  map_app_composition 3 4 7.
11. 1, 2, 6 ⊢ app g (app f a) = app (g ∘ f) a, eq_symm 9.
12. 1, 2, 6, 8 ⊢ app g (app f a) = app (g ∘ f) b, eq_trans 11 8.
13. 1, 2, 6, 7, 8 ⊢ app g (app f a) = app g (app f b), eq_trans 12 10.
14. 1, 6 ⊢ app f a ∈ Y, map_app_in_cod 3 6.
15. 1, 7 ⊢ app f b ∈ Y, map_app_in_cod 3 7.
16. 1, 2, 6, 7, 8 ⊢ app f a = app f b, inj_elim 2 14 15 13.
17. 1, 2, 6, 7, 8 ⊢ a = b, inj_elim 1 6 7 16.
18. 1, 2 ⊢ a ∈ X → b ∈ X →
  app (g ∘ f) a = app (g ∘ f) b → a = b, subj_intro_iii 17.
19. 1, 2 ⊢ ∀b. a ∈ X → b ∈ X →
  app (g ∘ f) a = app (g ∘ f) b → a = b, uq_intro 18.
20. 1, 2 ⊢ ∀a. ∀b. a ∈ X → b ∈ X →
  app (g ∘ f) a = app (g ∘ f) b → a = b, uq_intro 19.
21. 1, 2 ⊢ inj (g ∘ f) X Z, inj_intro 5 20.
composition_inj_inj_is_inj. ⊢ inj f X Y → inj g Y Z → inj (g ∘ f) X Z,
  subj_intro_ii 21.

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