Theorem ffsrn

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

	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		cnvexg	⊢ ( 𝐹 ∈ 𝑉 → ◡ 𝐹 ∈ V )
31		imaexg	⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ V )
32	2 30 31	3syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ V )
33		cnvimass	⊢ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ dom 𝐹
34		fores	⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) : ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) –onto→ ( 𝐹 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
35	3 33 34	sylancl	⊢ ( 𝜑 → ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) : ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) –onto→ ( 𝐹 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
36		fofn	⊢ ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) : ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) –onto→ ( 𝐹 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) Fn ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
37	35 36	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) Fn ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
38		fnrndomg	⊢ ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ V → ( ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) Fn ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) → ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ≼ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
39	32 37 38	sylc	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ≼ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
40		domfi	⊢ ( ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin ∧ ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ≼ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) → ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
41	29 39 40	syl2anc	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
42		snfi	⊢ { 𝑍 } ∈ Fin
43		df-ima	⊢ ( 𝐹 “ ( ◡ 𝐹 “ { 𝑍 } ) ) = ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) )
44		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑍 } ) ) = ( { 𝑍 } ∩ ran 𝐹 ) )
45	3 44	syl	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑍 } ) ) = ( { 𝑍 } ∩ ran 𝐹 ) )
46	43 45	eqtr3id	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) = ( { 𝑍 } ∩ ran 𝐹 ) )
47		inss1	⊢ ( { 𝑍 } ∩ ran 𝐹 ) ⊆ { 𝑍 }
48	46 47	eqsstrdi	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ⊆ { 𝑍 } )
49		ssfi	⊢ ( ( { 𝑍 } ∈ Fin ∧ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ⊆ { 𝑍 } ) → ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ∈ Fin )
50	42 48 49	sylancr	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ∈ Fin )
51		unfi	⊢ ( ( ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin ∧ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ∈ Fin ) → ( ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ) ∈ Fin )
52	41 50 51	syl2anc	⊢ ( 𝜑 → ( ran ( 𝐹 ↾ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ∪ ran ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) ) ∈ Fin )
53	26 52	eqeltrd	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )