Theorem dprdffsupp

Description: A finitely supported function in S is a finitely supported function. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

	Ref	Expression
Hypotheses	dprdff.w	|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
	dprdff.1	|- ( ph -> G dom DProd S )
	dprdff.2	|- ( ph -> dom S = I )
	dprdff.3	|- ( ph -> F e. W )
Assertion	dprdffsupp	|- ( ph -> F finSupp .0. )

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
2		dprdff.1	|- ( ph -> G dom DProd S )
3		dprdff.2	|- ( ph -> dom S = I )
4		dprdff.3	|- ( ph -> F e. W )
5	1 2 3	dprdw	|- ( ph -> ( F e. W <-> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) ) )
6	4 5	mpbid	|- ( ph -> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) )
7	6	simp3d	|- ( ph -> F finSupp .0. )