This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )