Metamath Proof Explorer

Theorem elsetpreimafvssdm

Description: An element of the class P of all preimages of function values is a subset of the domain of the function. (Contributed by AV, 8-Mar-2024)

		Ref	Expression
	Hypothesis	setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
	Assertion	elsetpreimafvssdm	$⊢ (F Fn A \land S \in P) \to S \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2	1	elsetpreimafv	$⊢ S \in P \to \exists x \in A S = F^{-1} [\{F (x)\}]$
3		cnvimass	$⊢ F^{-1} [\{F (x)\}] \subseteq dom F$
4		fndm	$⊢ F Fn A \to dom F = A$
5	3 4	sseqtrid	$⊢ F Fn A \to F^{-1} [\{F (x)\}] \subseteq A$
6	5	adantr	$⊢ (F Fn A \land x \in A) \to F^{-1} [\{F (x)\}] \subseteq A$
7		sseq1	$⊢ S = F^{-1} [\{F (x)\}] \to (S \subseteq A \leftrightarrow F^{-1} [\{F (x)\}] \subseteq A)$
8	6 7	syl5ibrcom	$⊢ (F Fn A \land x \in A) \to (S = F^{-1} [\{F (x)\}] \to S \subseteq A)$
9	8	expcom	$⊢ x \in A \to (F Fn A \to (S = F^{-1} [\{F (x)\}] \to S \subseteq A))$
10	9	com23	$⊢ x \in A \to (S = F^{-1} [\{F (x)\}] \to (F Fn A \to S \subseteq A))$
11	10	rexlimiv	$⊢ \exists x \in A S = F^{-1} [\{F (x)\}] \to (F Fn A \to S \subseteq A)$
12	2 11	syl	$⊢ S \in P \to (F Fn A \to S \subseteq A)$
13	12	impcom	$⊢ (F Fn A \land S \in P) \to S \subseteq A$