Theorem fimacnvdisj

Description: The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007)

	Ref	Expression
Assertion	fimacnvdisj	$$⊢\left(F:A⟶B\wedge B\cap C=\varnothing \right)\to F^{-1}\left[C\right]=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}F=\mathrm{dom}{F}^{-1}$$
2		frn	$$⊢F:A⟶B\to \mathrm{ran}F\subseteq B$$
3	2	adantr	$$⊢\left(F:A⟶B\wedge B\cap C=\varnothing \right)\to \mathrm{ran}F\subseteq B$$
4	1 3	eqsstrrid	$$⊢\left(F:A⟶B\wedge B\cap C=\varnothing \right)\to \mathrm{dom}{F}^{-1}\subseteq B$$
5		ssdisj	$$⊢\left(\mathrm{dom}{F}^{-1}\subseteq B\wedge B\cap C=\varnothing \right)\to \mathrm{dom}{F}^{-1}\cap C=\varnothing$$
6	4 5	sylancom	$$⊢\left(F:A⟶B\wedge B\cap C=\varnothing \right)\to \mathrm{dom}{F}^{-1}\cap C=\varnothing$$
7		imadisj	$$⊢F^{-1}\left[C\right]=\varnothing \leftrightarrow \mathrm{dom}{F}^{-1}\cap C=\varnothing$$
8	6 7	sylibr	$$⊢\left(F:A⟶B\wedge B\cap C=\varnothing \right)\to F^{-1}\left[C\right]=\varnothing$$