Theorem indicator_is_map

Proof
01. ⊢ set ∅, empty_set_is_set.
02. ⊢ set {∅}, set_sg 1.
03. ⊢ ∅ ∈ {∅, {∅}}, in21 1.
04. ⊢ {∅} ∈ {∅, {∅}}, in22 2.
05. 5 ⊢ x ∈ X \ A, hypo.
06. 6 ⊢ x ∈ A, hypo.
07. 5 ⊢ ∅ ∈ {∅, {∅}}, wk 3.
08. 6 ⊢ {∅} ∈ {∅, {∅}}, wk 4.
09. ⊢ x ∈ X \ A → ∅ ∈ {∅, {∅}}, subj_intro 7.
10. ⊢ x ∈ A → {∅} ∈ {∅, {∅}}, subj_intro 8.
11. ⊢ ∀x. x ∈ X \ A → ∅ ∈ {∅, {∅}}, uq_intro 9.
12. ⊢ ∀x. x ∈ A → {∅} ∈ {∅, {∅}}, uq_intro 10.
13. ⊢ {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)}
  = {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)}, eq_refl.
14. ⊢ {t | ∃x. x ∈ A ∧ t = (x, {∅})}
  = {t | ∃x. x ∈ A ∧ t = (x, {∅})}, eq_refl.
15. ⊢ map {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)} (X \ A) {∅, {∅}},
  map_from_term 13 11.
16. ⊢ map {t | ∃x. x ∈ A ∧ t = (x, {∅})} A {∅, {∅}},
  map_from_term 14 12.
17. ⊢ A ∩ (X \ A) = ∅, intersection_rel_compl.
18. ⊢ (X \ A) ∩ A = A ∩ (X \ A), intersection_comm.
19. ⊢ (X \ A) ∩ A = ∅, eq_trans 18 17.
20. ⊢ map ({t | ∃x. x ∈ X \ A ∧ t = (x, ∅)} ∪
  {t | ∃x. x ∈ A ∧ t = (x, {∅})}) ((X \ A) ∪ A) {∅, {∅}},
  map_union_eq_rngs 15 16 19.
21. ⊢ map (χ A X) ((X \ A) ∪ A) {∅, {∅}},
  eq_subst_rev indicator_eq 20, P t ↔ map t ((X \ A) ∪ A) {∅, {∅}}.
22. 22 ⊢ A ⊆ X, hypo.
23. 22 ⊢ (X \ A) ∪ A = X, diff_union_subclass 22.
24. 22 ⊢ map (χ A X) X {∅, {∅}},
  eq_subst 23 21, P t ↔ map (χ A X) t {∅, {∅}}.
indicator_is_map. ⊢ A ⊆ X → map (χ A X) X {∅, {∅}}, subj_intro 24.

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