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		df-ss	$⊢ F [A] \subseteq B \leftrightarrow \forall y (y \in F [A] \to y \in B)$
2		vex	$⊢ y \in V$
3	2	elima	$⊢ y \in F [A] \leftrightarrow \exists x \in A x F y$
4		eqcom	$⊢ y = F (x) \leftrightarrow F (x) = y$
5		ssel	$⊢ A \subseteq dom F \to (x \in A \to x \in dom F)$
6		funbrfvb	$⊢ (Fun F \land x \in dom F) \to (F (x) = y \leftrightarrow x F y)$
7	6	ex	$⊢ Fun F \to (x \in dom F \to (F (x) = y \leftrightarrow x F y))$
8	5 7	syl9	$⊢ A \subseteq dom F \to (Fun F \to (x \in A \to (F (x) = y \leftrightarrow x F y)))$
9	8	imp31	$⊢ ((A \subseteq dom F \land Fun F) \land x \in A) \to (F (x) = y \leftrightarrow x F y)$
10	4 9	bitrid	$⊢ ((A \subseteq dom F \land Fun F) \land x \in A) \to (y = F (x) \leftrightarrow x F y)$
11	10	rexbidva	$⊢ (A \subseteq dom F \land Fun F) \to (\exists x \in A y = F (x) \leftrightarrow \exists x \in A x F y)$
12	3 11	bitr4id	$⊢ (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	bitr4di	$⊢ (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	bitrdi	$⊢ (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	bitrid	$⊢ (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