funimassd

Description: Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Step	Hyp	Ref	Expression
1		funimassd.1	$⊢ Ⅎ x φ$
2		funimassd.2	$⊢ φ \to Fun F$
3		funimassd.3	$⊢ (φ \land x \in A) \to F (x) \in B$
4		fvelima	$⊢ (Fun F \land y \in F [A]) \to \exists x \in A F (x) = y$
5	2 4	sylan	$⊢ (φ \land y \in F [A]) \to \exists x \in A F (x) = y$
6		nfv	$⊢ Ⅎ x y \in F [A]$
7	1 6	nfan	$⊢ Ⅎ x (φ \land y \in F [A])$
8		nfv	$⊢ Ⅎ x y \in B$
9		id	$⊢ F (x) = y \to F (x) = y$
10	9	eqcomd	$⊢ F (x) = y \to y = F (x)$
11	10	3ad2ant3	$⊢ (φ \land x \in A \land F (x) = y) \to y = F (x)$
12	3	3adant3	$⊢ (φ \land x \in A \land F (x) = y) \to F (x) \in B$
13	11 12	eqeltrd	$⊢ (φ \land x \in A \land F (x) = y) \to y \in B$
14	13	3exp	$⊢ φ \to (x \in A \to (F (x) = y \to y \in B))$
15	14	adantr	$⊢ (φ \land y \in F [A]) \to (x \in A \to (F (x) = y \to y \in B))$
16	7 8 15	rexlimd	$⊢ (φ \land y \in F [A]) \to (\exists x \in A F (x) = y \to y \in B)$
17	5 16	mpd	$⊢ (φ \land y \in F [A]) \to y \in B$
18	17	ex	$⊢ φ \to (y \in F [A] \to y \in B)$
19	18	ssrdv	$⊢ φ \to F [A] \subseteq B$

Metamath Proof Explorer