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 ⊢ φ → Z ∈ W
ffsrn.0 ⊢ φ → F ∈ V
ffsrn.1 ⊢ φ → Fun ⁡ F
ffsrn.2 ⊢ φ → F supp Z ∈ Fin
Assertion ffsrn ⊢ φ → ran ⁡ F ∈ Fin

Proof

Step Hyp Ref Expression
1 ffsrn.z ⊢ φ → Z ∈ W
2 ffsrn.0 ⊢ φ → F ∈ V
3 ffsrn.1 ⊢ φ → Fun ⁡ F
4 ffsrn.2 ⊢ φ → F supp Z ∈ Fin
5 imaundi ⊢ F -1 V ∖ Z ∪ Z = F -1 V ∖ Z ∪ F -1 Z
6 5 reseq2i ⊢ F ↾ F -1 V ∖ Z ∪ Z = F ↾ F -1 V ∖ Z ∪ F -1 Z
7 undif1 ⊢ V ∖ Z ∪ Z = V ∪ Z
8 ssv ⊢ Z ⊆ V
9 ssequn2 ⊢ Z ⊆ V ↔ V ∪ Z = V
10 8 9 mpbi ⊢ V ∪ Z = V
11 7 10 eqtri ⊢ V ∖ Z ∪ Z = V
12 11 imaeq2i ⊢ F -1 V ∖ Z ∪ Z = F -1 V
13 12 reseq2i ⊢ F ↾ F -1 V ∖ Z ∪ Z = F ↾ F -1 V
14 resundi ⊢ F ↾ F -1 V ∖ Z ∪ F -1 Z = F ↾ F -1 V ∖ Z ∪ F ↾ F -1 Z
15 6 13 14 3eqtr3i ⊢ F ↾ F -1 V = F ↾ F -1 V ∖ Z ∪ F ↾ F -1 Z
16 dfdm4 ⊢ dom ⁡ F = ran ⁡ F -1
17 dfrn4 ⊢ ran ⁡ F -1 = F -1 V
18 16 17 eqtri ⊢ dom ⁡ F = F -1 V
19 df-fn ⊢ F Fn F -1 V ↔ Fun ⁡ F ∧ dom ⁡ F = F -1 V
20 fnresdm ⊢ F Fn F -1 V → F ↾ F -1 V = F
21 19 20 sylbir ⊢ Fun ⁡ F ∧ dom ⁡ F = F -1 V → F ↾ F -1 V = F
22 3 18 21 sylancl ⊢ φ → F ↾ F -1 V = F
23 15 22 syl5reqr ⊢ φ → F = F ↾ F -1 V ∖ Z ∪ F ↾ F -1 Z
24 23 rneqd ⊢ φ → ran ⁡ F = ran ⁡ F ↾ F -1 V ∖ Z ∪ F ↾ F -1 Z
25 rnun ⊢ ran ⁡ F ↾ F -1 V ∖ Z ∪ F ↾ F -1 Z = ran ⁡ F ↾ F -1 V ∖ Z ∪ ran ⁡ F ↾ F -1 Z
26 24 25 syl6eq ⊢ φ → ran ⁡ F = ran ⁡ F ↾ F -1 V ∖ Z ∪ ran ⁡ F ↾ F -1 Z
27 suppimacnv ⊢ F ∈ V ∧ Z ∈ W → F supp Z = F -1 V ∖ Z
28 2 1 27 syl2anc ⊢ φ → F supp Z = F -1 V ∖ Z
29 28 4 eqeltrrd ⊢ φ → F -1 V ∖ Z ∈ Fin
30 cnvexg ⊢ F ∈ V → F -1 ∈ V
31 imaexg ⊢ F -1 ∈ V → F -1 V ∖ Z ∈ V
32 2 30 31 3syl ⊢ φ → F -1 V ∖ Z ∈ V
33 cnvimass ⊢ F -1 V ∖ Z ⊆ dom ⁡ F
34 fores ⊢ Fun ⁡ F ∧ F -1 V ∖ Z ⊆ dom ⁡ F → F ↾ F -1 V ∖ Z : F -1 V ∖ Z ⟶ onto F F -1 V ∖ Z
35 3 33 34 sylancl ⊢ φ → F ↾ F -1 V ∖ Z : F -1 V ∖ Z ⟶ onto F F -1 V ∖ Z
36 fofn ⊢ F ↾ F -1 V ∖ Z : F -1 V ∖ Z ⟶ onto F F -1 V ∖ Z → F ↾ F -1 V ∖ Z Fn F -1 V ∖ Z
37 35 36 syl ⊢ φ → F ↾ F -1 V ∖ Z Fn F -1 V ∖ Z
38 fnrndomg ⊢ F -1 V ∖ Z ∈ V → F ↾ F -1 V ∖ Z Fn F -1 V ∖ Z → ran ⁡ F ↾ F -1 V ∖ Z ≼ F -1 V ∖ Z
39 32 37 38 sylc ⊢ φ → ran ⁡ F ↾ F -1 V ∖ Z ≼ F -1 V ∖ Z
40 domfi ⊢ F -1 V ∖ Z ∈ Fin ∧ ran ⁡ F ↾ F -1 V ∖ Z ≼ F -1 V ∖ Z → ran ⁡ F ↾ F -1 V ∖ Z ∈ Fin
41 29 39 40 syl2anc ⊢ φ → ran ⁡ F ↾ F -1 V ∖ Z ∈ Fin
42 snfi ⊢ Z ∈ Fin
43 df-ima ⊢ F F -1 Z = ran ⁡ F ↾ F -1 Z
44 funimacnv ⊢ Fun ⁡ F → F F -1 Z = Z ∩ ran ⁡ F
45 3 44 syl ⊢ φ → F F -1 Z = Z ∩ ran ⁡ F
46 43 45 syl5eqr ⊢ φ → ran ⁡ F ↾ F -1 Z = Z ∩ ran ⁡ F
47 inss1 ⊢ Z ∩ ran ⁡ F ⊆ Z
48 46 47 eqsstrdi ⊢ φ → ran ⁡ F ↾ F -1 Z ⊆ Z
49 ssfi ⊢ Z ∈ Fin ∧ ran ⁡ F ↾ F -1 Z ⊆ Z → ran ⁡ F ↾ F -1 Z ∈ Fin
50 42 48 49 sylancr ⊢ φ → ran ⁡ F ↾ F -1 Z ∈ Fin
51 unfi ⊢ ran ⁡ F ↾ F -1 V ∖ Z ∈ Fin ∧ ran ⁡ F ↾ F -1 Z ∈ Fin → ran ⁡ F ↾ F -1 V ∖ Z ∪ ran ⁡ F ↾ F -1 Z ∈ Fin
52 41 50 51 syl2anc ⊢ φ → ran ⁡ F ↾ F -1 V ∖ Z ∪ ran ⁡ F ↾ F -1 Z ∈ Fin
53 26 52 eqeltrd ⊢ φ → ran ⁡ F ∈ Fin