Theorem id_neutl

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ x ∈ X, hypo.
03. ⊢ map (id Y) Y Y, id_is_map.
04. 1, 2 ⊢ app f x ∈ Y, map_app_in_cod 1 2.
05. 1, 2 ⊢ app (id Y) (app f x) = app f x, id_app 4.
06. 1, 2 ⊢ app (id Y ∘ f) x = app (id Y) (app f x),
  map_app_composition 1 3 2.
07. 1, 2 ⊢ app (id Y ∘ f) x = app f x, eq_trans 6 5.
08. 1 ⊢ x ∈ X → app (id Y ∘ f) x = app f x, subj_intro 7.
09. 1 ⊢ ∀x. x ∈ X → app (id Y ∘ f) x = app f x, uq_intro 8.
10. 1 ⊢ map (id Y ∘ f) X Y, composition_is_map 1 3.
11. 1 ⊢ id Y ∘ f = f, map_extensionality 10 1 9.
id_neutl. ⊢ map f X Y → id Y ∘ f = f, subj_intro 11.

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