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	$⊢ (F : A ⟶ B \land B \cap C = \emptyset) \to F^{-1} [C] = \emptyset$

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

Metamath Proof Explorer