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 𝑍 )
fsuppres.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion fsuppres ( 𝜑 → ( 𝐹 ↾ 𝑋 ) finSupp 𝑍 )

Proof

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