Theorem ffsrn

Description: The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017)

	Ref	Expression
Hypotheses	ffsrn.z	$$⊢\phi \to Z\in W$$
	ffsrn.0	$$⊢\phi \to F\in V$$
	ffsrn.1	$$⊢\phi \to \mathrm{Fun}F$$
	ffsrn.2	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$
Assertion	ffsrn	$$⊢\phi \to \mathrm{ran}F\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		ffsrn.z	$$⊢\phi \to Z\in W$$
2		ffsrn.0	$$⊢\phi \to F\in V$$
3		ffsrn.1	$$⊢\phi \to \mathrm{Fun}F$$
4		ffsrn.2	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$
5		dfdm4	$$⊢\mathrm{dom}F=\mathrm{ran}{F}^{-1}$$
6		dfrn4	$$⊢\mathrm{ran}{F}^{-1}=F^{-1}\left[\mathrm{V}\right]$$
7	5 6	eqtri	$$⊢\mathrm{dom}F=F^{-1}\left[\mathrm{V}\right]$$
8		df-fn	$$⊢FFn{F}^{-1}\left[\mathrm{V}\right]\leftrightarrow \left(\mathrm{Fun}F\wedge \mathrm{dom}F=F^{-1}\left[\mathrm{V}\right]\right)$$
9		fnresdm	$$⊢FFn{F}^{-1}\left[\mathrm{V}\right]\to {F\upharpoonright }_{F^{-1}\left[\mathrm{V}\right]}=F$$
10	8 9	sylbir	$$⊢\left(\mathrm{Fun}F\wedge \mathrm{dom}F=F^{-1}\left[\mathrm{V}\right]\right)\to {F\upharpoonright }_{F^{-1}\left[\mathrm{V}\right]}=F$$
11	3 7 10	sylancl	$$⊢\phi \to {F\upharpoonright }_{F^{-1}\left[\mathrm{V}\right]}=F$$
12		imaundi	$$⊢F^{-1}\left[\left(\mathrm{V}\setminus \left\{Z\right\}\right)\cup \left\{Z\right\}\right]=F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\cup F^{-1}\left[\left\{Z\right\}\right]$$
13	12	reseq2i	$$⊢{F\upharpoonright }_{F^{-1}\left[\left(\mathrm{V}\setminus \left\{Z\right\}\right)\cup \left\{Z\right\}\right]}={F\upharpoonright }_{\left(F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\cup F^{-1}\left[\left\{Z\right\}\right]\right)}$$
14		undif1	$$⊢\left(\mathrm{V}\setminus \left\{Z\right\}\right)\cup \left\{Z\right\}=\mathrm{V}\cup \left\{Z\right\}$$
15		ssv	$$⊢\left\{Z\right\}\subseteq \mathrm{V}$$
16		ssequn2	$$⊢\left\{Z\right\}\subseteq \mathrm{V}\leftrightarrow \mathrm{V}\cup \left\{Z\right\}=\mathrm{V}$$
17	15 16	mpbi	$$⊢\mathrm{V}\cup \left\{Z\right\}=\mathrm{V}$$
18	14 17	eqtri	$$⊢\left(\mathrm{V}\setminus \left\{Z\right\}\right)\cup \left\{Z\right\}=\mathrm{V}$$
19	18	imaeq2i	$$⊢F^{-1}\left[\left(\mathrm{V}\setminus \left\{Z\right\}\right)\cup \left\{Z\right\}\right]=F^{-1}\left[\mathrm{V}\right]$$
20	19	reseq2i	$$⊢{F\upharpoonright }_{F^{-1}\left[\left(\mathrm{V}\setminus \left\{Z\right\}\right)\cup \left\{Z\right\}\right]}={F\upharpoonright }_{F^{-1}\left[\mathrm{V}\right]}$$
21		resundi	$$⊢{F\upharpoonright }_{\left(F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\cup F^{-1}\left[\left\{Z\right\}\right]\right)}=\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)$$
22	13 20 21	3eqtr3i	$$⊢{F\upharpoonright }_{F^{-1}\left[\mathrm{V}\right]}=\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)$$
23	11 22	eqtr3di	$$⊢\phi \to F=\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)$$
24	23	rneqd	$$⊢\phi \to \mathrm{ran}F=\mathrm{ran}\left(\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\right)$$
25		rnun	$$⊢\mathrm{ran}\left(\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\right)=\mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)$$
26	24 25	eqtrdi	$$⊢\phi \to \mathrm{ran}F=\mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)$$
27		suppimacnv	$$⊢\left(F\in V\wedge Z\in W\right)\to F\mathrm{supp}Z=F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
28	2 1 27	syl2anc	$$⊢\phi \to F\mathrm{supp}Z=F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
29	28 4	eqeltrrd	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$
30		cnvexg	$$⊢F\in V\to F^{-1}\in \mathrm{V}$$
31		imaexg	$$⊢F^{-1}\in \mathrm{V}\to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{V}$$
32	2 30 31	3syl	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{V}$$
33		cnvimass	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\subseteq \mathrm{dom}F$$
34		fores	$$⊢\left(\mathrm{Fun}F\wedge F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\subseteq \mathrm{dom}F\right)\to \left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right):F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\underset{onto}{⟶}F\left[F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right]$$
35	3 33 34	sylancl	$$⊢\phi \to \left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right):F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\underset{onto}{⟶}F\left[F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right]$$
36		fofn	$$⊢\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right):F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\underset{onto}{⟶}F\left[F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right]\to \left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)Fn{F}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
37	35 36	syl	$$⊢\phi \to \left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)Fn{F}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
38		fnrndomg	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{V}\to \left(\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)Fn{F}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\preccurlyeq F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right)$$
39	32 37 38	sylc	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\preccurlyeq F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
40		domfi	$$⊢\left(F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}\wedge \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\preccurlyeq F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right)\to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\in \mathrm{Fin}$$
41	29 39 40	syl2anc	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\in \mathrm{Fin}$$
42		snfi	$$⊢\left\{Z\right\}\in \mathrm{Fin}$$
43		df-ima	$$⊢F\left[F^{-1}\left[\left\{Z\right\}\right]\right]=\mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)$$
44		funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[\left\{Z\right\}\right]\right]=\left\{Z\right\}\cap \mathrm{ran}F$$
45	3 44	syl	$$⊢\phi \to F\left[F^{-1}\left[\left\{Z\right\}\right]\right]=\left\{Z\right\}\cap \mathrm{ran}F$$
46	43 45	eqtr3id	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)=\left\{Z\right\}\cap \mathrm{ran}F$$
47		inss1	$$⊢\left\{Z\right\}\cap \mathrm{ran}F\subseteq \left\{Z\right\}$$
48	46 47	eqsstrdi	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\subseteq \left\{Z\right\}$$
49		ssfi	$$⊢\left(\left\{Z\right\}\in \mathrm{Fin}\wedge \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\subseteq \left\{Z\right\}\right)\to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\in \mathrm{Fin}$$
50	42 48 49	sylancr	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\in \mathrm{Fin}$$
51		unfi	$$⊢\left(\mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\in \mathrm{Fin}\wedge \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\in \mathrm{Fin}\right)\to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\in \mathrm{Fin}$$
52	41 50 51	syl2anc	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\cup \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\in \mathrm{Fin}$$
53	26 52	eqeltrd	$$⊢\phi \to \mathrm{ran}F\in \mathrm{Fin}$$