Theorem dmhashres

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

	Ref	Expression
Assertion	dmhashres	$$⊢\mathrm{dom}\left({\left|.\right|\upharpoonright }_A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		dmres	$$⊢\mathrm{dom}\left({\left|.\right|\upharpoonright }_A\right)=A\cap \mathrm{dom}\left|.\right|$$
2		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
3	2	fdmi	$$⊢\mathrm{dom}\left|.\right|=\mathrm{V}$$
4	3	ineq2i	$$⊢A\cap \mathrm{dom}\left|.\right|=A\cap \mathrm{V}$$
5		inv1	$$⊢A\cap \mathrm{V}=A$$
6	1 4 5	3eqtri	$$⊢\mathrm{dom}\left({\left|.\right|\upharpoonright }_A\right)=A$$