Proof 01. 1 ⊢ A ⊆ B, hypo. 02. 1 ⊢ A ∪ B = B, union_from_incl 1. 03. 1 ⊢ img R (A ∪ B) = img R B, f_equal 2, f u = img R u. 04. ⊢ img R A ∪ img R B = img R (A ∪ B), eq_symm img_dist_union. 05. 1 ⊢ img R A ∪ img R B = img R B, eq_trans 4 3. 06. 1 ⊢ img R A ⊆ img R B, incl_from_union 5. img_incl. ⊢ A ⊆ B → img R A ⊆ img R B, subj_intro 6.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.