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	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
	ffsrn.0	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	ffsrn.1	⊢ ( 𝜑 → Fun 𝐹 )
	ffsrn.2	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
Assertion	ffsrn	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		ffsrn.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
2		ffsrn.0	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		ffsrn.1	⊢ ( 𝜑 → Fun 𝐹 )
4		ffsrn.2	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
5		dfdm4	⊢ dom 𝐹 = ran ◡ 𝐹
6		dfrn4	⊢ ran ◡ 𝐹 = ( ◡ 𝐹 “ V )
7	5 6	eqtri	⊢ dom 𝐹 = ( ◡ 𝐹 “ V )
8		df-fn	⊢ ( 𝐹 Fn ( ◡ 𝐹 “ V ) ↔ ( Fun 𝐹 ∧ dom 𝐹 = ( ◡ 𝐹 “ V ) ) )
9		fnresdm	⊢ ( 𝐹 Fn ( ◡ 𝐹 “ V ) → ( 𝐹 ↾ ( ◡ 𝐹 “ V ) ) = 𝐹 )
10	8 9	sylbir	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 = ( ◡ 𝐹 “ V ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ V ) ) = 𝐹 )
11	3 7 10	sylancl	⊢ ( 𝜑 → ( 𝐹 ↾ ( ◡ 𝐹 “ V ) ) = 𝐹 )
12		imaundi	⊢ ( ◡ 𝐹 “ ( ( V ∖ { 𝑍 } ) ∪ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐹 “ { 𝑍 } ) )
13	12	reseq2i	⊢ ( 𝐹 ↾ ( ◡ 𝐹 “ ( ( V ∖ { 𝑍 } ) ∪ { 𝑍 } ) ) ) = ( 𝐹 ↾ ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐹 “ { 𝑍 } ) ) )
14		undif1	⊢ ( ( V ∖ { 𝑍 } ) ∪ { 𝑍 } ) = ( V ∪ { 𝑍 } )
15		ssv	⊢ { 𝑍 } ⊆ V
16		ssequn2	⊢ ( { 𝑍 } ⊆ V ↔ ( V ∪ { 𝑍 } ) = V )
17	15 16	mpbi	⊢ ( V ∪ { 𝑍 } ) = V
18	14 17	eqtri	⊢ ( ( V ∖ { 𝑍 } ) ∪ { 𝑍 } ) = V
19	18	imaeq2i	⊢ ( ◡ 𝐹 “ ( ( V ∖ { 𝑍 } ) ∪ { 𝑍 } ) ) = ( ◡ 𝐹 “ V )
20	19	reseq2i	⊢ ( 𝐹 ↾ ( ◡ 𝐹 “ ( ( V ∖ { 𝑍 } ) ∪ { 𝑍 } ) ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ V ) )
21		resundi	⊢ ( 𝐹 ↾ ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐹 “ { 𝑍 } ) ) ) = ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
22	13 20 21	3eqtr3i	⊢ ( 𝐹 ↾ ( ◡ 𝐹 “ V ) ) = ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
23	11 22	eqtr3di	⊢ ( 𝜑 → 𝐹 = ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ) )
24	23	rneqd	⊢ ( 𝜑 → ran 𝐹 = ran ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ) )
25		rnun	⊢ ran ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ) = ( ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
26	24 25	eqtrdi	⊢ ( 𝜑 → ran 𝐹 = ( ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ) )
27		suppimacnv	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
28	2 1 27	syl2anc	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
29	28 4	eqeltrrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
30		finnum	⊢ ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ dom card )
31	29 30	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ dom card )
32		cnvimass	⊢ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ dom 𝐹
33		fores	⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) : ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) –onto→ ( 𝐹 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
34	3 32 33	sylancl	⊢ ( 𝜑 → ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) : ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) –onto→ ( 𝐹 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
35		fofn	⊢ ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) : ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) –onto→ ( 𝐹 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) Fn ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
36	34 35	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) Fn ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
37		fnrndomnum	⊢ ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ dom card → ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) Fn ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) → ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ≼ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
38	31 36 37	sylc	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ≼ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
39		domfi	⊢ ( ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin ∧ ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ≼ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) → ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
40	29 38 39	syl2anc	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
41		snfi	⊢ { 𝑍 } ∈ Fin
42		df-ima	⊢ ( 𝐹 “ ( ◡ 𝐹 “ { 𝑍 } ) ) = ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) )
43		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑍 } ) ) = ( { 𝑍 } ∩ ran 𝐹 ) )
44	3 43	syl	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑍 } ) ) = ( { 𝑍 } ∩ ran 𝐹 ) )
45	42 44	eqtr3id	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) = ( { 𝑍 } ∩ ran 𝐹 ) )
46		inss1	⊢ ( { 𝑍 } ∩ ran 𝐹 ) ⊆ { 𝑍 }
47	45 46	eqsstrdi	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ⊆ { 𝑍 } )
48		ssfi	⊢ ( ( { 𝑍 } ∈ Fin ∧ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ⊆ { 𝑍 } ) → ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ∈ Fin )
49	41 47 48	sylancr	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ∈ Fin )
50		unfi	⊢ ( ( ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin ∧ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ∈ Fin ) → ( ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ) ∈ Fin )
51	40 49 50	syl2anc	⊢ ( 𝜑 → ( ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ) ∈ Fin )
52	26 51	eqeltrd	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )