Theorem fsupprnfi

Description: Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024)

	Ref	Expression
Assertion	fsupprnfi	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \mathrm{ran}F\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		snfi	$$⊢\left\{\underset{\dot{}}{0}\right\}\in \mathrm{Fin}$$
2		simpll	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \mathrm{Fun}F$$
3		simplr	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to F\in V$$
4		simprl	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \underset{\dot{}}{0}\in W$$
5		ressupprn	$$⊢\left(\mathrm{Fun}F\wedge F\in V\wedge \underset{\dot{}}{0}\in W\right)\to \mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)=\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}$$
6	2 3 4 5	syl3anc	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)=\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}$$
7		simprr	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
8	7	fsuppimpd	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
9		suppssdm	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{dom}F$$
10		ssdmres	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{dom}F\leftrightarrow \mathrm{dom}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)=F\mathrm{supp}\underset{\dot{}}{0}$$
11	9 10	mpbi	$$⊢\mathrm{dom}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)=F\mathrm{supp}\underset{\dot{}}{0}$$
12	2	funresd	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \mathrm{Fun}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)$$
13		funforn	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\leftrightarrow \left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right):\mathrm{dom}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)$$
14	12 13	sylib	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right):\mathrm{dom}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)$$
15		foeq2	$$⊢\mathrm{dom}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)=F\mathrm{supp}\underset{\dot{}}{0}\to \left(\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right):\mathrm{dom}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\leftrightarrow \left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right):F\mathrm{supp}\underset{\dot{}}{0}\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\right)$$
16	15	biimpa	$$⊢\left(\mathrm{dom}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)=F\mathrm{supp}\underset{\dot{}}{0}\wedge \left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right):\mathrm{dom}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\right)\to \left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right):F\mathrm{supp}\underset{\dot{}}{0}\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)$$
17	11 14 16	sylancr	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right):F\mathrm{supp}\underset{\dot{}}{0}\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)$$
18		fofi	$$⊢\left(F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\wedge \left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right):F\mathrm{supp}\underset{\dot{}}{0}\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\right)\to \mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\in \mathrm{Fin}$$
19	8 17 18	syl2anc	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \mathrm{ran}\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(F\right)}\right)\in \mathrm{Fin}$$
20	6 19	eqeltrrd	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{Fin}$$
21		diffib	$$⊢\left\{\underset{\dot{}}{0}\right\}\in \mathrm{Fin}\to \left(\mathrm{ran}F\in \mathrm{Fin}\leftrightarrow \mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{Fin}\right)$$
22	21	biimpar	$$⊢\left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{Fin}\wedge \mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{Fin}\right)\to \mathrm{ran}F\in \mathrm{Fin}$$
23	1 20 22	sylancr	$$⊢\left(\left(\mathrm{Fun}F\wedge F\in V\right)\wedge \left(\underset{\dot{}}{0}\in W\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to \mathrm{ran}F\in \mathrm{Fin}$$