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