respreima

Description: The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	respreima	$⊢ Fun F \to {({F ↾}_{B})}^{-1} [A] = F^{-1} [A] \cap B$

Proof

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2		elin	$⊢ x \in (B \cap dom F) \leftrightarrow (x \in B \land x \in dom F)$
3	2	biancomi	$⊢ x \in (B \cap dom F) \leftrightarrow (x \in dom F \land x \in B)$
4	3	anbi1i	$⊢ (x \in (B \cap dom F) \land ({F ↾}_{B}) (x) \in A) \leftrightarrow ((x \in dom F \land x \in B) \land ({F ↾}_{B}) (x) \in A)$
5		fvres	$⊢ x \in B \to ({F ↾}_{B}) (x) = F (x)$
6	5	eleq1d	$⊢ x \in B \to (({F ↾}_{B}) (x) \in A \leftrightarrow F (x) \in A)$
7	6	adantl	$⊢ (x \in dom F \land x \in B) \to (({F ↾}_{B}) (x) \in A \leftrightarrow F (x) \in A)$
8	7	pm5.32i	$⊢ ((x \in dom F \land x \in B) \land ({F ↾}_{B}) (x) \in A) \leftrightarrow ((x \in dom F \land x \in B) \land F (x) \in A)$
9	4 8	bitri	$⊢ (x \in (B \cap dom F) \land ({F ↾}_{B}) (x) \in A) \leftrightarrow ((x \in dom F \land x \in B) \land F (x) \in A)$
10	9	a1i	$⊢ F Fn dom F \to ((x \in (B \cap dom F) \land ({F ↾}_{B}) (x) \in A) \leftrightarrow ((x \in dom F \land x \in B) \land F (x) \in A))$
11		an32	$⊢ ((x \in dom F \land x \in B) \land F (x) \in A) \leftrightarrow ((x \in dom F \land F (x) \in A) \land x \in B)$
12	10 11	bitrdi	$⊢ F Fn dom F \to ((x \in (B \cap dom F) \land ({F ↾}_{B}) (x) \in A) \leftrightarrow ((x \in dom F \land F (x) \in A) \land x \in B))$
13		fnfun	$⊢ F Fn dom F \to Fun F$
14		funres	$⊢ Fun F \to Fun ({F ↾}_{B})$
15	13 14	syl	$⊢ F Fn dom F \to Fun ({F ↾}_{B})$
16		dmres	$⊢ dom ({F ↾}_{B}) = B \cap dom F$
17		df-fn	$⊢ ({F ↾}_{B}) Fn (B \cap dom F) \leftrightarrow (Fun ({F ↾}_{B}) \land dom ({F ↾}_{B}) = B \cap dom F)$
18	15 16 17	sylanblrc	$⊢ F Fn dom F \to ({F ↾}_{B}) Fn (B \cap dom F)$
19		elpreima	$⊢ ({F ↾}_{B}) Fn (B \cap dom F) \to (x \in {({F ↾}_{B})}^{-1} [A] \leftrightarrow (x \in (B \cap dom F) \land ({F ↾}_{B}) (x) \in A))$
20	18 19	syl	$⊢ F Fn dom F \to (x \in {({F ↾}_{B})}^{-1} [A] \leftrightarrow (x \in (B \cap dom F) \land ({F ↾}_{B}) (x) \in A))$
21		elin	$⊢ x \in (F^{-1} [A] \cap B) \leftrightarrow (x \in F^{-1} [A] \land x \in B)$
22		elpreima	$⊢ F Fn dom F \to (x \in F^{-1} [A] \leftrightarrow (x \in dom F \land F (x) \in A))$
23	22	anbi1d	$⊢ F Fn dom F \to ((x \in F^{-1} [A] \land x \in B) \leftrightarrow ((x \in dom F \land F (x) \in A) \land x \in B))$
24	21 23	syl5bb	$⊢ F Fn dom F \to (x \in (F^{-1} [A] \cap B) \leftrightarrow ((x \in dom F \land F (x) \in A) \land x \in B))$
25	12 20 24	3bitr4d	$⊢ F Fn dom F \to (x \in {({F ↾}_{B})}^{-1} [A] \leftrightarrow x \in (F^{-1} [A] \cap B))$
26	1 25	sylbi	$⊢ Fun F \to (x \in {({F ↾}_{B})}^{-1} [A] \leftrightarrow x \in (F^{-1} [A] \cap B))$
27	26	eqrdv	$⊢ Fun F \to {({F ↾}_{B})}^{-1} [A] = F^{-1} [A] \cap B$

Metamath Proof Explorer

Theorem respreima

Proof