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