This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )