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 )

Metamath Proof Explorer

Theorem evlselvlem

Proof