Theorem fn_inv_img_dist_inter

Distribution law for the inverse image operation with respect to intersection.

Proof sketch
The inclusion f⁻¹[A ∩ B] ⊆ f⁻¹[A] ∩ f⁻¹[B] is universally valid for any relation f. Thus it suffices to show the converse inclusion
  f⁻¹[A] ∩ f⁻¹[B] ⊆ f⁻¹[A ∩ B].
So let x ∈ f⁻¹[A] ∩ f⁻¹[B], thus x ∈ f⁻¹[A] as well as x ∈ f⁻¹[B]. In this respect, a ∈ A with (x, a) ∈ f and b ∈ B with (x, b) ∈ f exist. However, because f is a function, a = b follows from (x, a) ∈ f and (x, b) ∈ f, since a functions's argument has a unique value. Accordingly, a ∈ B holds, meaning that a ∈ A ∩ B with (x, a) ∈ f, which witnesses that x ∈ f⁻¹[A ∩ B]. q.e.d.

Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ x ∈ inv_img f A ∩ inv_img f B, hypo.
03. 2 ⊢ x ∈ inv_img f A, intersection_eliml 2.
04. 2 ⊢ x ∈ inv_img f B, intersection_elimr 2.
05. 2 ⊢ ∃a. a ∈ A ∧ (x, a) ∈ f, inv_img_elim 3.
06. 2 ⊢ ∃b. b ∈ B ∧ (x, b) ∈ f, inv_img_elim 4.
07. 7 ⊢ a ∈ A ∧ (x, a) ∈ f, hypo.
08. 8 ⊢ b ∈ B ∧ (x, b) ∈ f, hypo.
09. 7 ⊢ a ∈ A, conj_eliml 7.
10. 8 ⊢ b ∈ B, conj_eliml 8.
11. 7 ⊢ (x, a) ∈ f, conj_elimr 7.
12. 8 ⊢ (x, b) ∈ f, conj_elimr 8.
13. 1, 7, 8 ⊢ a = b, fn_unique_value 1 11 12.
14. 1, 7, 8 ⊢ a ∈ B, eq_subst_rev 13 10, P t ↔ t ∈ B.
15. 1, 7, 8 ⊢ a ∈ A ∩ B, intersection_intro 9 14.
16. 1, 7, 8 ⊢ x ∈ inv_img f (A ∩ B), inv_img_intro 15 11.
17. 1, 2, 7 ⊢ x ∈ inv_img f (A ∩ B), ex_elim 6 16.
18. 1, 2 ⊢ x ∈ inv_img f (A ∩ B), ex_elim 5 17.
19. 1 ⊢ x ∈ inv_img f A ∩ inv_img f B →
  x ∈ inv_img f (A ∩ B), subj_intro 18.
20. 1 ⊢ ∀x. x ∈ inv_img f A ∩ inv_img f B →
  x ∈ inv_img f (A ∩ B), uq_intro 19.
21. 1 ⊢ inv_img f A ∩ inv_img f B ⊆ inv_img f (A ∩ B),
  incl_intro 20.
22. ⊢ inv_img f (A ∩ B) ⊆ inv_img f A ∩ inv_img f B,
  inv_img_dist_inter.
23. 1 ⊢ inv_img f (A ∩ B) = inv_img f A ∩ inv_img f B,
  incl_antisym 22 21.
fn_inv_img_dist_inter. ⊢ function f →
  inv_img f (A ∩ B) = inv_img f A ∩ inv_img f B,
  subj_intro 23.

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