Metamath Proof Explorer

Theorem preiman0

Description: The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024)

		Ref	Expression
	Assertion	preiman0	$⊢ (Fun F \land A \subseteq ran F \land A \neq \emptyset) \to F^{-1} [A] \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$⊢ ran F = dom F^{-1}$
2	1	ineq1i	$⊢ ran F \cap (A \cap ran F) = dom F^{-1} \cap (A \cap ran F)$
3		dfss2	$⊢ A \subseteq ran F \leftrightarrow A \cap ran F = A$
4	3	biimpi	$⊢ A \subseteq ran F \to A \cap ran F = A$
5	4	ineq2d	$⊢ A \subseteq ran F \to ran F \cap (A \cap ran F) = ran F \cap A$
6		sseqin2	$⊢ A \subseteq ran F \leftrightarrow ran F \cap A = A$
7	6	biimpi	$⊢ A \subseteq ran F \to ran F \cap A = A$
8	5 7	eqtrd	$⊢ A \subseteq ran F \to ran F \cap (A \cap ran F) = A$
9	8	3ad2ant2	$⊢ (Fun F \land A \subseteq ran F \land F^{-1} [A] = \emptyset) \to ran F \cap (A \cap ran F) = A$
10		fimacnvinrn	$⊢ Fun F \to F^{-1} [A] = F^{-1} [A \cap ran F]$
11	10	eqeq1d	$⊢ Fun F \to (F^{-1} [A] = \emptyset \leftrightarrow F^{-1} [A \cap ran F] = \emptyset)$
12	11	biimpa	$⊢ (Fun F \land F^{-1} [A] = \emptyset) \to F^{-1} [A \cap ran F] = \emptyset$
13	12	3adant2	$⊢ (Fun F \land A \subseteq ran F \land F^{-1} [A] = \emptyset) \to F^{-1} [A \cap ran F] = \emptyset$
14		imadisj	$⊢ F^{-1} [A \cap ran F] = \emptyset \leftrightarrow dom F^{-1} \cap (A \cap ran F) = \emptyset$
15	13 14	sylib	$⊢ (Fun F \land A \subseteq ran F \land F^{-1} [A] = \emptyset) \to dom F^{-1} \cap (A \cap ran F) = \emptyset$
16	2 9 15	3eqtr3a	$⊢ (Fun F \land A \subseteq ran F \land F^{-1} [A] = \emptyset) \to A = \emptyset$
17	16	3expia	$⊢ (Fun F \land A \subseteq ran F) \to (F^{-1} [A] = \emptyset \to A = \emptyset)$
18	17	necon3d	$⊢ (Fun F \land A \subseteq ran F) \to (A \neq \emptyset \to F^{-1} [A] \neq \emptyset)$
19	18	3impia	$⊢ (Fun F \land A \subseteq ran F \land A \neq \emptyset) \to F^{-1} [A] \neq \emptyset$