Metamath Proof Explorer

Theorem fsuppres

Description: The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019)

Ref Expression
Hypotheses fsuppres.s ⊢ φ → finSupp Z⁡ F
fsuppres.z ⊢ φ → Z ∈ V
Assertion fsuppres ⊢ φ → finSupp Z⁡ F ↾ X

Proof

Step Hyp Ref Expression
1 fsuppres.s ⊢ φ → finSupp Z⁡ F
2 fsuppres.z ⊢ φ → Z ∈ V
3 fsuppimp ⊢ finSupp Z⁡ F → Fun ⁡ F ∧ F supp Z ∈ Fin
4 relprcnfsupp ⊢ ¬ F ∈ V → ¬ finSupp Z⁡ F
5 4 con4i ⊢ finSupp Z⁡ F → F ∈ V
6 1 5 syl ⊢ φ → F ∈ V
7 6 2 jca ⊢ φ → F ∈ V ∧ Z ∈ V
8 7 adantr ⊢ φ ∧ Fun ⁡ F → F ∈ V ∧ Z ∈ V
9 ressuppss ⊢ F ∈ V ∧ Z ∈ V → F ↾ X supp Z ⊆ F supp Z
10 ssfi ⊢ F supp Z ∈ Fin ∧ F ↾ X supp Z ⊆ F supp Z → F ↾ X supp Z ∈ Fin
11 10 expcom ⊢ F ↾ X supp Z ⊆ F supp Z → F supp Z ∈ Fin → F ↾ X supp Z ∈ Fin
12 8 9 11 3syl ⊢ φ ∧ Fun ⁡ F → F supp Z ∈ Fin → F ↾ X supp Z ∈ Fin
13 12 expcom ⊢ Fun ⁡ F → φ → F supp Z ∈ Fin → F ↾ X supp Z ∈ Fin
14 13 com23 ⊢ Fun ⁡ F → F supp Z ∈ Fin → φ → F ↾ X supp Z ∈ Fin
15 14 imp ⊢ Fun ⁡ F ∧ F supp Z ∈ Fin → φ → F ↾ X supp Z ∈ Fin
16 3 15 syl ⊢ finSupp Z⁡ F → φ → F ↾ X supp Z ∈ Fin
17 1 16 mpcom ⊢ φ → F ↾ X supp Z ∈ Fin
18 funres ⊢ Fun ⁡ F → Fun ⁡ F ↾ X
19 18 adantr ⊢ Fun ⁡ F ∧ F supp Z ∈ Fin → Fun ⁡ F ↾ X
20 1 3 19 3syl ⊢ φ → Fun ⁡ F ↾ X
21 resexg ⊢ F ∈ V → F ↾ X ∈ V
22 1 5 21 3syl ⊢ φ → F ↾ X ∈ V
23 funisfsupp ⊢ Fun ⁡ F ↾ X ∧ F ↾ X ∈ V ∧ Z ∈ V → finSupp Z⁡ F ↾ X ↔ F ↾ X supp Z ∈ Fin
24 20 22 2 23 syl3anc ⊢ φ → finSupp Z⁡ F ↾ X ↔ F ↾ X supp Z ∈ Fin
25 17 24 mpbird ⊢ φ → finSupp Z⁡ F ↾ X