Theorem inj_from_left_inv

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ ∃g. map g Y X ∧ g ∘ f = id X, hypo.
03. 3 ⊢ map g Y X ∧ g ∘ f = id X, hypo.
04. 3 ⊢ map g Y X, conj_eliml 3.
05. 3 ⊢ g ∘ f = id X, conj_elimr 3.
06. 6 ⊢ a ∈ X, hypo.
07. 7 ⊢ b ∈ X, hypo.
08. 8 ⊢ app f a = app f b, hypo.
09. 8 ⊢ app g (app f a) = app g (app f b), f_equal 8, f x = app g x.
10. 1, 3, 6 ⊢ app (g ∘ f) a = app g (app f a), map_app_composition 1 4 6.
11. 1, 3, 7 ⊢ app (g ∘ f) b = app g (app f b), map_app_composition 1 4 7.
12. 1, 3, 6, 8 ⊢ app (g ∘ f) a = app g (app f b), eq_trans 10 9.
13. 1, 3, 7 ⊢ app g (app f b) = app (g ∘ f) b, eq_symm 11.
14. 1, 3, 6, 7, 8 ⊢ app (g ∘ f) a = app (g ∘ f) b, eq_trans 12 13.
15. 1, 3, 6, 7, 8 ⊢ app (id X) a = app (g ∘ f) b,
  eq_subst 5 14, P t ↔ app t a = app (g ∘ f) b.
16. 1, 3, 6, 7, 8 ⊢ app (id X) a = app (id X) b,
  eq_subst 5 15, P t ↔ app (id X) a = app t b.
17. 6 ⊢ app (id X) a = a, id_app 6.
18. 7 ⊢ app (id X) b = b, id_app 7.
19. 1, 3, 6, 7, 8 ⊢ app (id X) a = b, eq_trans 16 18.
20. 6 ⊢ a = app (id X) a, eq_symm 17.
21. 1, 3, 6, 7, 8 ⊢ a = b, eq_trans 20 19.
22. 1, 3 ⊢ a ∈ X → b ∈ X → app f a = app f b → a = b, subj_intro_iii 21.
23. 1, 3 ⊢ ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b, uq_intro 22.
24. 1, 3 ⊢ ∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b, uq_intro 23.
25. 1, 3 ⊢ inj f X Y, inj_intro 1 24.
26. 1, 2 ⊢ inj f X Y, ex_elim 2 25.
inj_from_left_inv. ⊢ map f X Y → (∃g. map g Y X ∧ g ∘ f = id X) →
  inj f X Y, subj_intro_ii 26.

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