Theorem resfifsupp

Description: The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019)

	Ref	Expression
Hypotheses	resfifsupp.f	⊢ ( 𝜑 → Fun 𝐹 )
	resfifsupp.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	resfifsupp.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion	resfifsupp	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑋 ) finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		resfifsupp.f	⊢ ( 𝜑 → Fun 𝐹 )
2		resfifsupp.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		resfifsupp.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4		resindm	⊢ ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝑋 )
5	1	funfnd	⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
6		fnresin2	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) Fn ( 𝑋 ∩ dom 𝐹 ) )
7	5 6	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) Fn ( 𝑋 ∩ dom 𝐹 ) )
8		infi	⊢ ( 𝑋 ∈ Fin → ( 𝑋 ∩ dom 𝐹 ) ∈ Fin )
9	2 8	syl	⊢ ( 𝜑 → ( 𝑋 ∩ dom 𝐹 ) ∈ Fin )
10	7 9 3	fndmfifsupp	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) finSupp 𝑍 )
11	4 10	eqbrtrrid	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑋 ) finSupp 𝑍 )