Theorem fsuppres

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

	Ref	Expression
Hypotheses	fsuppres.s	|- ( ph -> F finSupp Z )
	fsuppres.z	|- ( ph -> Z e. V )
Assertion	fsuppres	|- ( ph -> ( F |` X ) finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fsuppres.s	|- ( ph -> F finSupp Z )
2		fsuppres.z	|- ( ph -> Z e. V )
3		fsuppimp	|- ( F finSupp Z -> ( Fun F /\ ( F supp Z ) e. Fin ) )
4		relprcnfsupp	|- ( -. F e. _V -> -. F finSupp Z )
5	4	con4i	|- ( F finSupp Z -> F e. _V )
6	1 5	syl	|- ( ph -> F e. _V )
7	6 2	jca	|- ( ph -> ( F e. _V /\ Z e. V ) )
8	7	adantr	|- ( ( ph /\ Fun F ) -> ( F e. _V /\ Z e. V ) )
9		ressuppss	|- ( ( F e. _V /\ Z e. V ) -> ( ( F |` X ) supp Z ) C_ ( F supp Z ) )
10		ssfi	|- ( ( ( F supp Z ) e. Fin /\ ( ( F |` X ) supp Z ) C_ ( F supp Z ) ) -> ( ( F |` X ) supp Z ) e. Fin )
11	10	expcom	|- ( ( ( F |` X ) supp Z ) C_ ( F supp Z ) -> ( ( F supp Z ) e. Fin -> ( ( F |` X ) supp Z ) e. Fin ) )
12	8 9 11	3syl	|- ( ( ph /\ Fun F ) -> ( ( F supp Z ) e. Fin -> ( ( F |` X ) supp Z ) e. Fin ) )
13	12	expcom	|- ( Fun F -> ( ph -> ( ( F supp Z ) e. Fin -> ( ( F |` X ) supp Z ) e. Fin ) ) )
14	13	com23	|- ( Fun F -> ( ( F supp Z ) e. Fin -> ( ph -> ( ( F |` X ) supp Z ) e. Fin ) ) )
15	14	imp	|- ( ( Fun F /\ ( F supp Z ) e. Fin ) -> ( ph -> ( ( F |` X ) supp Z ) e. Fin ) )
16	3 15	syl	|- ( F finSupp Z -> ( ph -> ( ( F |` X ) supp Z ) e. Fin ) )
17	1 16	mpcom	|- ( ph -> ( ( F |` X ) supp Z ) e. Fin )
18		funres	|- ( Fun F -> Fun ( F |` X ) )
19	18	adantr	|- ( ( Fun F /\ ( F supp Z ) e. Fin ) -> Fun ( F |` X ) )
20	1 3 19	3syl	|- ( ph -> Fun ( F |` X ) )
21		resexg	|- ( F e. _V -> ( F |` X ) e. _V )
22	1 5 21	3syl	|- ( ph -> ( F |` X ) e. _V )
23		funisfsupp	|- ( ( Fun ( F |` X ) /\ ( F |` X ) e. _V /\ Z e. V ) -> ( ( F |` X ) finSupp Z <-> ( ( F |` X ) supp Z ) e. Fin ) )
24	20 22 2 23	syl3anc	|- ( ph -> ( ( F |` X ) finSupp Z <-> ( ( F |` X ) supp Z ) e. Fin ) )
25	17 24	mpbird	|- ( ph -> ( F |` X ) finSupp Z )