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		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
5	1 4	syl	⊢ ( 𝜑 → Rel 𝐹 )
6		resindm	⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝑋 ) )
7	5 6	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝑋 ) )
8	1	funfnd	⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
9		fnresin2	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) Fn ( 𝑋 ∩ dom 𝐹 ) )
10	8 9	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) Fn ( 𝑋 ∩ dom 𝐹 ) )
11		infi	⊢ ( 𝑋 ∈ Fin → ( 𝑋 ∩ dom 𝐹 ) ∈ Fin )
12	2 11	syl	⊢ ( 𝜑 → ( 𝑋 ∩ dom 𝐹 ) ∈ Fin )
13	10 12 3	fndmfifsupp	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) finSupp 𝑍 )
14	7 13	eqbrtrrd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑋 ) finSupp 𝑍 )