Theorem ffsrn

Description: The range of a finitely supported function is finite. The proof uses fnrndomnum rather than fnrndomg , and so does not require ax-ac . (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Vincent Gonzalez, 24-Aug-2026)

	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		finnum	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}\to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{dom}\mathrm{card}$$
31	29 30	syl	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{dom}\mathrm{card}$$
32		cnvimass	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\subseteq \mathrm{dom}F$$
33		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]$$
34	3 32 33	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]$$
35		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]$$
36	34 35	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]$$
37		fnrndomnum	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{dom}\mathrm{card}\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)$$
38	31 36 37	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]$$
39		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}$$
40	29 38 39	syl2anc	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]}\right)\in \mathrm{Fin}$$
41		snfi	$$⊢\left\{Z\right\}\in \mathrm{Fin}$$
42		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)$$
43		funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[\left\{Z\right\}\right]\right]=\left\{Z\right\}\cap \mathrm{ran}F$$
44	3 43	syl	$$⊢\phi \to F\left[F^{-1}\left[\left\{Z\right\}\right]\right]=\left\{Z\right\}\cap \mathrm{ran}F$$
45	42 44	eqtr3id	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)=\left\{Z\right\}\cap \mathrm{ran}F$$
46		inss1	$$⊢\left\{Z\right\}\cap \mathrm{ran}F\subseteq \left\{Z\right\}$$
47	45 46	eqsstrdi	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\subseteq \left\{Z\right\}$$
48		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}$$
49	41 47 48	sylancr	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{F^{-1}\left[\left\{Z\right\}\right]}\right)\in \mathrm{Fin}$$
50		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}$$
51	40 49 50	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}$$
52	26 51	eqeltrd	$$⊢\phi \to \mathrm{ran}F\in \mathrm{Fin}$$