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	bilani	$⊢ (Fun F \land ran F \subseteq B) \to B \cap ran F = ran F$
4	3	ineq2d	$⊢ (Fun F \land ran F \subseteq B) \to A \cap (B \cap ran F) = A \cap ran F$
5	1 4	eqtrid	$⊢ (Fun F \land ran F \subseteq B) \to (A \cap B) \cap ran F = A \cap ran F$
6	5	imaeq2d	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [(A \cap B) \cap ran F] = F^{-1} [A \cap ran F]$
7		fimacnvinrn	$⊢ Fun F \to F^{-1} [A \cap B] = F^{-1} [(A \cap B) \cap ran F]$
8	7	adantr	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [A \cap B] = F^{-1} [(A \cap B) \cap ran F]$
9		fimacnvinrn	$⊢ Fun F \to F^{-1} [A] = F^{-1} [A \cap ran F]$
10	9	adantr	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [A] = F^{-1} [A \cap ran F]$
11	6 8 10	3eqtr4rd	$⊢ (Fun F \land ran F \subseteq B) \to F^{-1} [A] = F^{-1} [A \cap B]$

Metamath Proof Explorer