Theorem psrbagres

Description: Restrict a bag of variables in I to a bag of variables in J C_ I . (Contributed by SN, 10-Mar-2025)

	Ref	Expression
Hypotheses	psrbagres.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	psrbagres.e	|- E = { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin }
	psrbagres.i	|- ( ph -> I e. V )
	psrbagres.j	|- ( ph -> J C_ I )
	psrbagres.f	|- ( ph -> F e. D )
Assertion	psrbagres	|- ( ph -> ( F |` J ) e. E )

Proof

Step	Hyp	Ref	Expression
1		psrbagres.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
2		psrbagres.e	|- E = { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin }
3		psrbagres.i	|- ( ph -> I e. V )
4		psrbagres.j	|- ( ph -> J C_ I )
5		psrbagres.f	|- ( ph -> F e. D )
6	1	psrbagf	|- ( F e. D -> F : I --> NN0 )
7	5 6	syl	|- ( ph -> F : I --> NN0 )
8	7 4	fssresd	|- ( ph -> ( F |` J ) : J --> NN0 )
9	1	psrbagfsupp	|- ( F e. D -> F finSupp 0 )
10	5 9	syl	|- ( ph -> F finSupp 0 )
11		0zd	|- ( ph -> 0 e. ZZ )
12	10 11	fsuppres	|- ( ph -> ( F |` J ) finSupp 0 )
13	5	resexd	|- ( ph -> ( F |` J ) e. _V )
14		fcdmnn0fsuppg	|- ( ( ( F |` J ) e. _V /\ ( F |` J ) : J --> NN0 ) -> ( ( F |` J ) finSupp 0 <-> ( `' ( F |` J ) " NN ) e. Fin ) )
15	13 8 14	syl2anc	|- ( ph -> ( ( F |` J ) finSupp 0 <-> ( `' ( F |` J ) " NN ) e. Fin ) )
16	12 15	mpbid	|- ( ph -> ( `' ( F |` J ) " NN ) e. Fin )
17	3 4	ssexd	|- ( ph -> J e. _V )
18	2	psrbag	|- ( J e. _V -> ( ( F |` J ) e. E <-> ( ( F |` J ) : J --> NN0 /\ ( `' ( F |` J ) " NN ) e. Fin ) ) )
19	17 18	syl	|- ( ph -> ( ( F |` J ) e. E <-> ( ( F |` J ) : J --> NN0 /\ ( `' ( F |` J ) " NN ) e. Fin ) ) )
20	8 16 19	mpbir2and	|- ( ph -> ( F |` J ) e. E )