funimass4

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006)

		Ref	Expression
	Assertion	funimass4	$⊢ (Fun F \land A \subseteq dom F) \to (F [A] \subseteq B \leftrightarrow \forall x \in A F (x) \in B)$

Proof

Step	Hyp	Ref	Expression
1		dfss2	$⊢ F [A] \subseteq B \leftrightarrow \forall y (y \in F [A] \to y \in B)$
2		eqcom	$⊢ y = F (x) \leftrightarrow F (x) = y$
3		ssel	$⊢ A \subseteq dom F \to (x \in A \to x \in dom F)$
4		funbrfvb	$⊢ (Fun F \land x \in dom F) \to (F (x) = y \leftrightarrow x F y)$
5	4	ex	$⊢ Fun F \to (x \in dom F \to (F (x) = y \leftrightarrow x F y))$
6	3 5	syl9	$⊢ A \subseteq dom F \to (Fun F \to (x \in A \to (F (x) = y \leftrightarrow x F y)))$
7	6	imp31	$⊢ ((A \subseteq dom F \land Fun F) \land x \in A) \to (F (x) = y \leftrightarrow x F y)$
8	2 7	syl5bb	$⊢ ((A \subseteq dom F \land Fun F) \land x \in A) \to (y = F (x) \leftrightarrow x F y)$
9	8	rexbidva	$⊢ (A \subseteq dom F \land Fun F) \to (\exists x \in A y = F (x) \leftrightarrow \exists x \in A x F y)$
10		vex	$⊢ y \in V$
11	10	elima	$⊢ y \in F [A] \leftrightarrow \exists x \in A x F y$
12	9 11	syl6rbbr	$⊢ (A \subseteq dom F \land Fun F) \to (y \in F [A] \leftrightarrow \exists x \in A y = F (x))$
13	12	imbi1d	$⊢ (A \subseteq dom F \land Fun F) \to ((y \in F [A] \to y \in B) \leftrightarrow (\exists x \in A y = F (x) \to y \in B))$
14		r19.23v	$⊢ \forall x \in A (y = F (x) \to y \in B) \leftrightarrow (\exists x \in A y = F (x) \to y \in B)$
15	13 14	syl6bbr	$⊢ (A \subseteq dom F \land Fun F) \to ((y \in F [A] \to y \in B) \leftrightarrow \forall x \in A (y = F (x) \to y \in B))$
16	15	albidv	$⊢ (A \subseteq dom F \land Fun F) \to (\forall y (y \in F [A] \to y \in B) \leftrightarrow \forall y \forall x \in A (y = F (x) \to y \in B))$
17		ralcom4	$⊢ \forall x \in A \forall y (y = F (x) \to y \in B) \leftrightarrow \forall y \forall x \in A (y = F (x) \to y \in B)$
18		fvex	$⊢ F (x) \in V$
19		eleq1	$⊢ y = F (x) \to (y \in B \leftrightarrow F (x) \in B)$
20	18 19	ceqsalv	$⊢ \forall y (y = F (x) \to y \in B) \leftrightarrow F (x) \in B$
21	20	ralbii	$⊢ \forall x \in A \forall y (y = F (x) \to y \in B) \leftrightarrow \forall x \in A F (x) \in B$
22	17 21	bitr3i	$⊢ \forall y \forall x \in A (y = F (x) \to y \in B) \leftrightarrow \forall x \in A F (x) \in B$
23	16 22	syl6bb	$⊢ (A \subseteq dom F \land Fun F) \to (\forall y (y \in F [A] \to y \in B) \leftrightarrow \forall x \in A F (x) \in B)$
24	1 23	syl5bb	$⊢ (A \subseteq dom F \land Fun F) \to (F [A] \subseteq B \leftrightarrow \forall x \in A F (x) \in B)$
25	24	ancoms	$⊢ (Fun F \land A \subseteq dom F) \to (F [A] \subseteq B \leftrightarrow \forall x \in A F (x) \in B)$

Metamath Proof Explorer

Theorem funimass4

Proof