fimacnvinrn2

Description: Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017)

		Ref	Expression
	Assertion	fimacnvinrn2	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [A] = F^{-1} [A \cap B]$

Step	Hyp	Ref	Expression
1		inass	$⊢ (A \cap B) \cap ran F = A \cap (B \cap ran F)$
2		sseqin2	$⊢ ran F \subseteq B \leftrightarrow B \cap ran F = ran F$
3	2	biimpi	$⊢ ran F \subseteq B \to B \cap ran F = ran F$
4	3	adantl	$⊢ (Fun F \land ran F \subseteq B) \to B \cap ran F = ran F$
5	4	ineq2d	$⊢ (Fun F \land ran F \subseteq B) \to A \cap (B \cap ran F) = A \cap ran F$
6	1 5	syl5eq	$⊢ (Fun F \land ran F \subseteq B) \to (A \cap B) \cap ran F = A \cap ran F$
7	6	imaeq2d	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [(A \cap B) \cap ran F] = F^{-1} [A \cap ran F]$
8		fimacnvinrn	$⊢ Fun F \to F^{-1} [A \cap B] = F^{-1} [(A \cap B) \cap ran F]$
9	8	adantr	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [A \cap B] = F^{-1} [(A \cap B) \cap ran F]$
10		fimacnvinrn	$⊢ Fun F \to F^{-1} [A] = F^{-1} [A \cap ran F]$
11	10	adantr	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [A] = F^{-1} [A \cap ran F]$
12	7 9 11	3eqtr4rd	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [A] = F^{-1} [A \cap B]$

Metamath Proof Explorer