Proof 01. 1 ⊢ A ⊆ X, hypo. 02. 2 ⊢ y ∈ img (id X) A, hypo. 03. 2 ⊢ ∃x. x ∈ A ∧ (x, y) ∈ id X, img_elim 2. 04. 4 ⊢ x ∈ A ∧ (x, y) ∈ id X, hypo. 05. 4 ⊢ x ∈ A, conj_eliml 4. 06. 4 ⊢ (x, y) ∈ id X, conj_elimr 4. 07. 4 ⊢ y = app (id X) x, map_app_intro id_is_map 6. 08. 1, 4 ⊢ x ∈ X, incl_elim 1 5. 09. 1, 4 ⊢ app (id X) x = x, id_app 8. 10. 1, 4 ⊢ y = x, eq_trans 7 9. 11. 1, 4 ⊢ y ∈ A, eq_subst_rev 10 5. 12. 1, 2 ⊢ y ∈ A, ex_elim 3 11. 13. 1 ⊢ y ∈ img (id X) A → y ∈ A, subj_intro 12. 14. 14 ⊢ y ∈ A, hypo. 15. 1, 14 ⊢ y ∈ X, incl_elim 1 14. 16. 1, 14 ⊢ app (id X) y = y, id_app 15. 17. 1, 14 ⊢ y = app (id X) y, eq_symm 16. 18. 1, 14 ⊢ (y, y) ∈ id X, map_app_elim id_is_map 15 17. 19. 1, 14 ⊢ y ∈ img (id X) A, img_intro 14 18. 20. 1 ⊢ y ∈ A → y ∈ img (id X) A, subj_intro 19. 21. 1 ⊢ y ∈ img (id X) A ↔ y ∈ A, bij_intro 13 20. 22. 1 ⊢ ∀y. y ∈ img (id X) A ↔ y ∈ A, uq_intro 21. 23. 1 ⊢ img (id X) A = A, ext 22. id_img. ⊢ A ⊆ X → img (id X) A = A, subj_intro 23.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.