Theorem hashresfn

Description: Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Assertion	hashresfn	$$⊢\left({\left|.\right|\upharpoonright }_A\right)FnA$$

Proof

Step	Hyp	Ref	Expression
1		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
2		ffn	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\to \left|.\right|Fn\mathrm{V}$$
3		fnresin2	$$⊢\left|.\right|Fn\mathrm{V}\to \left({\left|.\right|\upharpoonright }_{\left(A\cap \mathrm{V}\right)}\right)Fn\left(A\cap \mathrm{V}\right)$$
4	1 2 3	mp2b	$$⊢\left({\left|.\right|\upharpoonright }_{\left(A\cap \mathrm{V}\right)}\right)Fn\left(A\cap \mathrm{V}\right)$$
5		inv1	$$⊢A\cap \mathrm{V}=A$$
6	5	reseq2i	$$⊢{\left|.\right|\upharpoonright }_{\left(A\cap \mathrm{V}\right)}={\left|.\right|\upharpoonright }_A$$
7		fneq12	$$⊢\left({\left|.\right|\upharpoonright }_{\left(A\cap \mathrm{V}\right)}={\left|.\right|\upharpoonright }_A\wedge A\cap \mathrm{V}=A\right)\to \left(\left({\left|.\right|\upharpoonright }_{\left(A\cap \mathrm{V}\right)}\right)Fn\left(A\cap \mathrm{V}\right)\leftrightarrow \left({\left|.\right|\upharpoonright }_A\right)FnA\right)$$
8	6 5 7	mp2an	$$⊢\left({\left|.\right|\upharpoonright }_{\left(A\cap \mathrm{V}\right)}\right)Fn\left(A\cap \mathrm{V}\right)\leftrightarrow \left({\left|.\right|\upharpoonright }_A\right)FnA$$
9	4 8	mpbi	$$⊢\left({\left|.\right|\upharpoonright }_A\right)FnA$$