Theorem id_neutr

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

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