Metamath Proof Explorer

Theorem evlselvlem

Description: Lemma for evlselv . Used to re-index to and from bags of variables in I and bags of variables in the subsets J and I \ J . (Contributed by SN, 10-Mar-2025)

Ref Expression
Hypotheses evlselvlem.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlselvlem.e 
|- E = { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin }
evlselvlem.c 
|- C = { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin }
evlselvlem.h 
|- H = ( c e. C , e e. E |-> ( c u. e ) )
evlselvlem.i 
|- ( ph -> I e. V )
evlselvlem.j 
|- ( ph -> J C_ I )
Assertion evlselvlem 
|- ( ph -> H : ( C X. E ) -1-1-onto-> D )

Proof

Step Hyp Ref Expression
1 evlselvlem.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
2 evlselvlem.e 
 |-  E = { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin }
3 evlselvlem.c 
 |-  C = { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin }
4 evlselvlem.h 
 |-  H = ( c e. C , e e. E |-> ( c u. e ) )
5 evlselvlem.i 
 |-  ( ph -> I e. V )
6 evlselvlem.j 
 |-  ( ph -> J C_ I )
7 undifr 
 |-  ( J C_ I <-> ( ( I \ J ) u. J ) = I )
8 6 7 sylib 
 |-  ( ph -> ( ( I \ J ) u. J ) = I )
9 8 adantr 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( ( I \ J ) u. J ) = I )
10 3 psrbagf 
 |-  ( c e. C -> c : ( I \ J ) --> NN0 )
11 10 ad2antrl 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> c : ( I \ J ) --> NN0 )
12 2 psrbagf 
 |-  ( e e. E -> e : J --> NN0 )
13 12 ad2antll 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> e : J --> NN0 )
14 disjdifr 
 |-  ( ( I \ J ) i^i J ) = (/)
15 14 a1i 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( ( I \ J ) i^i J ) = (/) )
16 11 13 15 fun2d 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( c u. e ) : ( ( I \ J ) u. J ) --> NN0 )
17 9 16 feq2dd 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( c u. e ) : I --> NN0 )
18 unexg 
 |-  ( ( c e. C /\ e e. E ) -> ( c u. e ) e. _V )
19 18 adantl 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( c u. e ) e. _V )
20 0zd 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> 0 e. ZZ )
21 16 ffund 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> Fun ( c u. e ) )
22 3 psrbagfsupp 
 |-  ( c e. C -> c finSupp 0 )
23 22 ad2antrl 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> c finSupp 0 )
24 2 psrbagfsupp 
 |-  ( e e. E -> e finSupp 0 )
25 24 ad2antll 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> e finSupp 0 )
26 23 25 fsuppun 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( ( c u. e ) supp 0 ) e. Fin )
27 19 20 21 26 isfsuppd 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( c u. e ) finSupp 0 )
28 fcdmnn0fsuppg 
 |-  ( ( ( c u. e ) e. _V /\ ( c u. e ) : ( ( I \ J ) u. J ) --> NN0 ) -> ( ( c u. e ) finSupp 0 <-> ( `' ( c u. e ) " NN ) e. Fin ) )
29 19 16 28 syl2anc 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( ( c u. e ) finSupp 0 <-> ( `' ( c u. e ) " NN ) e. Fin ) )
30 27 29 mpbid 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( `' ( c u. e ) " NN ) e. Fin )
31 5 adantr 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> I e. V )
32 1 psrbag 
 |-  ( I e. V -> ( ( c u. e ) e. D <-> ( ( c u. e ) : I --> NN0 /\ ( `' ( c u. e ) " NN ) e. Fin ) ) )
33 31 32 syl 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( ( c u. e ) e. D <-> ( ( c u. e ) : I --> NN0 /\ ( `' ( c u. e ) " NN ) e. Fin ) ) )
34 17 30 33 mpbir2and 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( c u. e ) e. D )
35 5 adantr 
 |-  ( ( ph /\ d e. D ) -> I e. V )
36 difssd 
 |-  ( ( ph /\ d e. D ) -> ( I \ J ) C_ I )
37 simpr 
 |-  ( ( ph /\ d e. D ) -> d e. D )
38 1 3 35 36 37 psrbagres 
 |-  ( ( ph /\ d e. D ) -> ( d |` ( I \ J ) ) e. C )
39 6 adantr 
 |-  ( ( ph /\ d e. D ) -> J C_ I )
40 1 2 35 39 37 psrbagres 
 |-  ( ( ph /\ d e. D ) -> ( d |` J ) e. E )
41 1 psrbagf 
 |-  ( d e. D -> d : I --> NN0 )
42 41 adantl 
 |-  ( ( ph /\ d e. D ) -> d : I --> NN0 )
43 42 freld 
 |-  ( ( ph /\ d e. D ) -> Rel d )
44 42 fdmd 
 |-  ( ( ph /\ d e. D ) -> dom d = I )
45 39 7 sylib 
 |-  ( ( ph /\ d e. D ) -> ( ( I \ J ) u. J ) = I )
46 44 45 eqtr4d 
 |-  ( ( ph /\ d e. D ) -> dom d = ( ( I \ J ) u. J ) )
47 reldmun 
 |-  ( ( Rel d /\ dom d = ( ( I \ J ) u. J ) ) -> d = ( ( d |` ( I \ J ) ) u. ( d |` J ) ) )
48 43 46 47 syl2anc 
 |-  ( ( ph /\ d e. D ) -> d = ( ( d |` ( I \ J ) ) u. ( d |` J ) ) )
49 48 adantrl 
 |-  ( ( ph /\ ( ( c e. C /\ e e. E ) /\ d e. D ) ) -> d = ( ( d |` ( I \ J ) ) u. ( d |` J ) ) )
50 uneq12 
 |-  ( ( c = ( d |` ( I \ J ) ) /\ e = ( d |` J ) ) -> ( c u. e ) = ( ( d |` ( I \ J ) ) u. ( d |` J ) ) )
51 50 eqeq2d 
 |-  ( ( c = ( d |` ( I \ J ) ) /\ e = ( d |` J ) ) -> ( d = ( c u. e ) <-> d = ( ( d |` ( I \ J ) ) u. ( d |` J ) ) ) )
52 49 51 syl5ibrcom 
 |-  ( ( ph /\ ( ( c e. C /\ e e. E ) /\ d e. D ) ) -> ( ( c = ( d |` ( I \ J ) ) /\ e = ( d |` J ) ) -> d = ( c u. e ) ) )
53 11 ffnd 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> c Fn ( I \ J ) )
54 13 ffnd 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> e Fn J )
55 fnunres1 
 |-  ( ( c Fn ( I \ J ) /\ e Fn J /\ ( ( I \ J ) i^i J ) = (/) ) -> ( ( c u. e ) |` ( I \ J ) ) = c )
56 53 54 15 55 syl3anc 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( ( c u. e ) |` ( I \ J ) ) = c )
57 56 eqcomd 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> c = ( ( c u. e ) |` ( I \ J ) ) )
58 fnunres2 
 |-  ( ( c Fn ( I \ J ) /\ e Fn J /\ ( ( I \ J ) i^i J ) = (/) ) -> ( ( c u. e ) |` J ) = e )
59 53 54 15 58 syl3anc 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( ( c u. e ) |` J ) = e )
60 59 eqcomd 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> e = ( ( c u. e ) |` J ) )
61 57 60 jca 
 |-  ( ( ph /\ ( c e. C /\ e e. E ) ) -> ( c = ( ( c u. e ) |` ( I \ J ) ) /\ e = ( ( c u. e ) |` J ) ) )
62 61 adantrr 
 |-  ( ( ph /\ ( ( c e. C /\ e e. E ) /\ d e. D ) ) -> ( c = ( ( c u. e ) |` ( I \ J ) ) /\ e = ( ( c u. e ) |` J ) ) )
63 reseq1 
 |-  ( d = ( c u. e ) -> ( d |` ( I \ J ) ) = ( ( c u. e ) |` ( I \ J ) ) )
64 63 eqeq2d 
 |-  ( d = ( c u. e ) -> ( c = ( d |` ( I \ J ) ) <-> c = ( ( c u. e ) |` ( I \ J ) ) ) )
65 reseq1 
 |-  ( d = ( c u. e ) -> ( d |` J ) = ( ( c u. e ) |` J ) )
66 65 eqeq2d 
 |-  ( d = ( c u. e ) -> ( e = ( d |` J ) <-> e = ( ( c u. e ) |` J ) ) )
67 64 66 anbi12d 
 |-  ( d = ( c u. e ) -> ( ( c = ( d |` ( I \ J ) ) /\ e = ( d |` J ) ) <-> ( c = ( ( c u. e ) |` ( I \ J ) ) /\ e = ( ( c u. e ) |` J ) ) ) )
68 62 67 syl5ibrcom 
 |-  ( ( ph /\ ( ( c e. C /\ e e. E ) /\ d e. D ) ) -> ( d = ( c u. e ) -> ( c = ( d |` ( I \ J ) ) /\ e = ( d |` J ) ) ) )
69 52 68 impbid 
 |-  ( ( ph /\ ( ( c e. C /\ e e. E ) /\ d e. D ) ) -> ( ( c = ( d |` ( I \ J ) ) /\ e = ( d |` J ) ) <-> d = ( c u. e ) ) )
70 4 34 38 40 69 mpof1o2d 
 |-  ( ph -> H : ( C X. E ) -1-1-onto-> D )