funfvima

Description: A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003)

		Ref	Expression
	Assertion	funfvima	$⊢ (Fun F \land B \in dom F) \to (B \in A \to F (B) \in F [A])$

Step	Hyp	Ref	Expression
1		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
2	1	elin2	$⊢ B \in dom ({F ↾}_{A}) \leftrightarrow (B \in A \land B \in dom F)$
3		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
4		fvelrn	$⊢ (Fun ({F ↾}_{A}) \land B \in dom ({F ↾}_{A})) \to ({F ↾}_{A}) (B) \in ran ({F ↾}_{A})$
5	3 4	sylan	$⊢ (Fun F \land B \in dom ({F ↾}_{A})) \to ({F ↾}_{A}) (B) \in ran ({F ↾}_{A})$
6		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
7	6	eleq2i	$⊢ F (B) \in F [A] \leftrightarrow F (B) \in ran ({F ↾}_{A})$
8		fvres	$⊢ B \in A \to ({F ↾}_{A}) (B) = F (B)$
9	8	eleq1d	$⊢ B \in A \to (({F ↾}_{A}) (B) \in ran ({F ↾}_{A}) \leftrightarrow F (B) \in ran ({F ↾}_{A}))$
10	7 9	bitr4id	$⊢ B \in A \to (F (B) \in F [A] \leftrightarrow ({F ↾}_{A}) (B) \in ran ({F ↾}_{A}))$
11	5 10	syl5ibrcom	$⊢ (Fun F \land B \in dom ({F ↾}_{A})) \to (B \in A \to F (B) \in F [A])$
12	11	ex	$⊢ Fun F \to (B \in dom ({F ↾}_{A}) \to (B \in A \to F (B) \in F [A]))$
13	2 12	biimtrrid	$⊢ Fun F \to ((B \in A \land B \in dom F) \to (B \in A \to F (B) \in F [A]))$
14	13	expd	$⊢ Fun F \to (B \in A \to (B \in dom F \to (B \in A \to F (B) \in F [A])))$
15	14	com12	$⊢ B \in A \to (Fun F \to (B \in dom F \to (B \in A \to F (B) \in F [A])))$
16	15	impd	$⊢ B \in A \to ((Fun F \land B \in dom F) \to (B \in A \to F (B) \in F [A]))$
17	16	pm2.43b	$⊢ (Fun F \land B \in dom F) \to (B \in A \to F (B) \in F [A])$

Metamath Proof Explorer