afvres

Description: The value of a restricted function, analogous to fvres . (Contributed by Alexander van der Vekens, 22-Jul-2017)

		Ref	Expression
	Assertion	afvres	$⊢ A \in B \to (({F ↾}_{B})''' A) = (F''' A)$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ A \in (B \cap dom F) \leftrightarrow (A \in B \land A \in dom F)$
2	1	biimpri	$⊢ (A \in B \land A \in dom F) \to A \in (B \cap dom F)$
3		dmres	$⊢ dom ({F ↾}_{B}) = B \cap dom F$
4	2 3	eleqtrrdi	$⊢ (A \in B \land A \in dom F) \to A \in dom ({F ↾}_{B})$
5	4	ex	$⊢ A \in B \to (A \in dom F \to A \in dom ({F ↾}_{B}))$
6		snssi	$⊢ A \in B \to \{A\} \subseteq B$
7	6	resabs1d	$⊢ A \in B \to {({F ↾}_{B}) ↾}_{\{A\}} = {F ↾}_{\{A\}}$
8	7	eqcomd	$⊢ A \in B \to {F ↾}_{\{A\}} = {({F ↾}_{B}) ↾}_{\{A\}}$
9	8	funeqd	$⊢ A \in B \to (Fun ({F ↾}_{\{A\}}) \leftrightarrow Fun ({({F ↾}_{B}) ↾}_{\{A\}}))$
10	9	biimpd	$⊢ A \in B \to (Fun ({F ↾}_{\{A\}}) \to Fun ({({F ↾}_{B}) ↾}_{\{A\}}))$
11	5 10	anim12d	$⊢ A \in B \to ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \to (A \in dom ({F ↾}_{B}) \land Fun ({({F ↾}_{B}) ↾}_{\{A\}})))$
12	11	impcom	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to (A \in dom ({F ↾}_{B}) \land Fun ({({F ↾}_{B}) ↾}_{\{A\}}))$
13		df-dfat	$⊢ ({F ↾}_{B}) defAt A \leftrightarrow (A \in dom ({F ↾}_{B}) \land Fun ({({F ↾}_{B}) ↾}_{\{A\}}))$
14		afvfundmfveq	$⊢ ({F ↾}_{B}) defAt A \to (({F ↾}_{B})''' A) = ({F ↾}_{B}) (A)$
15	13 14	sylbir	$⊢ (A \in dom ({F ↾}_{B}) \land Fun ({({F ↾}_{B}) ↾}_{\{A\}})) \to (({F ↾}_{B})''' A) = ({F ↾}_{B}) (A)$
16	12 15	syl	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to (({F ↾}_{B})''' A) = ({F ↾}_{B}) (A)$
17		fvres	$⊢ A \in B \to ({F ↾}_{B}) (A) = F (A)$
18	17	adantl	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to ({F ↾}_{B}) (A) = F (A)$
19		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
20		afvfundmfveq	$⊢ F defAt A \to (F''' A) = F (A)$
21	19 20	sylbir	$⊢ (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to (F''' A) = F (A)$
22	21	eqcomd	$⊢ (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to F (A) = (F''' A)$
23	22	adantr	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to F (A) = (F''' A)$
24	16 18 23	3eqtrd	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to (({F ↾}_{B})''' A) = (F''' A)$
25		pm3.4	$⊢ (A \in B \land A \in dom F) \to (A \in B \to A \in dom F)$
26	1 25	sylbi	$⊢ A \in (B \cap dom F) \to (A \in B \to A \in dom F)$
27	26 3	eleq2s	$⊢ A \in dom ({F ↾}_{B}) \to (A \in B \to A \in dom F)$
28	27	com12	$⊢ A \in B \to (A \in dom ({F ↾}_{B}) \to A \in dom F)$
29	7	funeqd	$⊢ A \in B \to (Fun ({({F ↾}_{B}) ↾}_{\{A\}}) \leftrightarrow Fun ({F ↾}_{\{A\}}))$
30	29	biimpd	$⊢ A \in B \to (Fun ({({F ↾}_{B}) ↾}_{\{A\}}) \to Fun ({F ↾}_{\{A\}}))$
31	28 30	anim12d	$⊢ A \in B \to ((A \in dom ({F ↾}_{B}) \land Fun ({({F ↾}_{B}) ↾}_{\{A\}})) \to (A \in dom F \land Fun ({F ↾}_{\{A\}})))$
32	31	con3d	$⊢ A \in B \to (\neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to \neg (A \in dom ({F ↾}_{B}) \land Fun ({({F ↾}_{B}) ↾}_{\{A\}})))$
33	32	impcom	$⊢ (\neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to \neg (A \in dom ({F ↾}_{B}) \land Fun ({({F ↾}_{B}) ↾}_{\{A\}}))$
34		afvnfundmuv	$⊢ \neg ({F ↾}_{B}) defAt A \to (({F ↾}_{B})''' A) = V$
35	13 34	sylnbir	$⊢ \neg (A \in dom ({F ↾}_{B}) \land Fun ({({F ↾}_{B}) ↾}_{\{A\}})) \to (({F ↾}_{B})''' A) = V$
36	33 35	syl	$⊢ (\neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to (({F ↾}_{B})''' A) = V$
37		afvnfundmuv	$⊢ \neg F defAt A \to (F''' A) = V$
38	19 37	sylnbir	$⊢ \neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to (F''' A) = V$
39	38	eqcomd	$⊢ \neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to V = (F''' A)$
40	39	adantr	$⊢ (\neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to V = (F''' A)$
41	36 40	eqtrd	$⊢ (\neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \land A \in B) \to (({F ↾}_{B})''' A) = (F''' A)$
42	24 41	pm2.61ian	$⊢ A \in B \to (({F ↾}_{B})''' A) = (F''' A)$

Metamath Proof Explorer

Theorem afvres

Proof