Theorem sticksstones18

Description: Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones18.1	|- ( ph -> N e. NN0 )
	sticksstones18.2	|- ( ph -> K e. NN0 )
	sticksstones18.3	|- A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
	sticksstones18.4	|- B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
	sticksstones18.5	|- ( ph -> Z : ( 1 ... K ) -1-1-onto-> S )
	sticksstones18.6	|- F = ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) )
Assertion	sticksstones18	|- ( ph -> F : A --> B )

Proof

Step	Hyp	Ref	Expression
1		sticksstones18.1	|- ( ph -> N e. NN0 )
2		sticksstones18.2	|- ( ph -> K e. NN0 )
3		sticksstones18.3	|- A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
4		sticksstones18.4	|- B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
5		sticksstones18.5	|- ( ph -> Z : ( 1 ... K ) -1-1-onto-> S )
6		sticksstones18.6	|- F = ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) )
7	3	eqimssi	|- A C_ { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
8	7	a1i	|- ( ph -> A C_ { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } )
9	8	sseld	|- ( ph -> ( a e. A -> a e. { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } ) )
10	9	imp	|- ( ( ph /\ a e. A ) -> a e. { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } )
11		vex	|- a e. _V
12		feq1	|- ( g = a -> ( g : ( 1 ... K ) --> NN0 <-> a : ( 1 ... K ) --> NN0 ) )
13		simpl	|- ( ( g = a /\ i e. ( 1 ... K ) ) -> g = a )
14	13	fveq1d	|- ( ( g = a /\ i e. ( 1 ... K ) ) -> ( g ` i ) = ( a ` i ) )
15	14	sumeq2dv	|- ( g = a -> sum_ i e. ( 1 ... K ) ( g ` i ) = sum_ i e. ( 1 ... K ) ( a ` i ) )
16	15	eqeq1d	|- ( g = a -> ( sum_ i e. ( 1 ... K ) ( g ` i ) = N <-> sum_ i e. ( 1 ... K ) ( a ` i ) = N ) )
17	12 16	anbi12d	|- ( g = a -> ( ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) <-> ( a : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( a ` i ) = N ) ) )
18	11 17	elab	|- ( a e. { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } <-> ( a : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( a ` i ) = N ) )
19	10 18	sylib	|- ( ( ph /\ a e. A ) -> ( a : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( a ` i ) = N ) )
20	19	simpld	|- ( ( ph /\ a e. A ) -> a : ( 1 ... K ) --> NN0 )
21	20	adantr	|- ( ( ( ph /\ a e. A ) /\ x e. S ) -> a : ( 1 ... K ) --> NN0 )
22		f1ocnv	|- ( Z : ( 1 ... K ) -1-1-onto-> S -> `' Z : S -1-1-onto-> ( 1 ... K ) )
23	5 22	syl	|- ( ph -> `' Z : S -1-1-onto-> ( 1 ... K ) )
24		f1of	|- ( `' Z : S -1-1-onto-> ( 1 ... K ) -> `' Z : S --> ( 1 ... K ) )
25	23 24	syl	|- ( ph -> `' Z : S --> ( 1 ... K ) )
26	25	adantr	|- ( ( ph /\ a e. A ) -> `' Z : S --> ( 1 ... K ) )
27	26	ffvelrnda	|- ( ( ( ph /\ a e. A ) /\ x e. S ) -> ( `' Z ` x ) e. ( 1 ... K ) )
28	21 27	ffvelrnd	|- ( ( ( ph /\ a e. A ) /\ x e. S ) -> ( a ` ( `' Z ` x ) ) e. NN0 )
29	28	fmpttd	|- ( ( ph /\ a e. A ) -> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) : S --> NN0 )
30		eqidd	|- ( ( ( ph /\ a e. A ) /\ i e. S ) -> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) = ( x e. S |-> ( a ` ( `' Z ` x ) ) ) )
31		simpr	|- ( ( ( ( ph /\ a e. A ) /\ i e. S ) /\ x = i ) -> x = i )
32	31	fveq2d	|- ( ( ( ( ph /\ a e. A ) /\ i e. S ) /\ x = i ) -> ( `' Z ` x ) = ( `' Z ` i ) )
33	32	fveq2d	|- ( ( ( ( ph /\ a e. A ) /\ i e. S ) /\ x = i ) -> ( a ` ( `' Z ` x ) ) = ( a ` ( `' Z ` i ) ) )
34		simpr	|- ( ( ( ph /\ a e. A ) /\ i e. S ) -> i e. S )
35		fvexd	|- ( ( ( ph /\ a e. A ) /\ i e. S ) -> ( a ` ( `' Z ` i ) ) e. _V )
36	30 33 34 35	fvmptd	|- ( ( ( ph /\ a e. A ) /\ i e. S ) -> ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) = ( a ` ( `' Z ` i ) ) )
37	36	sumeq2dv	|- ( ( ph /\ a e. A ) -> sum_ i e. S ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) = sum_ i e. S ( a ` ( `' Z ` i ) ) )
38		fveq2	|- ( n = ( `' Z ` i ) -> ( a ` n ) = ( a ` ( `' Z ` i ) ) )
39		fzfid	|- ( ( ph /\ a e. A ) -> ( 1 ... K ) e. Fin )
40	5	adantr	|- ( ( ph /\ a e. A ) -> Z : ( 1 ... K ) -1-1-onto-> S )
41		f1oenfi	|- ( ( ( 1 ... K ) e. Fin /\ Z : ( 1 ... K ) -1-1-onto-> S ) -> ( 1 ... K ) ~~ S )
42	39 40 41	syl2anc	|- ( ( ph /\ a e. A ) -> ( 1 ... K ) ~~ S )
43	42	ensymd	|- ( ( ph /\ a e. A ) -> S ~~ ( 1 ... K ) )
44		enfii	|- ( ( ( 1 ... K ) e. Fin /\ S ~~ ( 1 ... K ) ) -> S e. Fin )
45	39 43 44	syl2anc	|- ( ( ph /\ a e. A ) -> S e. Fin )
46	23	adantr	|- ( ( ph /\ a e. A ) -> `' Z : S -1-1-onto-> ( 1 ... K ) )
47		eqidd	|- ( ( ( ph /\ a e. A ) /\ i e. S ) -> ( `' Z ` i ) = ( `' Z ` i ) )
48		nn0sscn	|- NN0 C_ CC
49	48	a1i	|- ( ( ph /\ a e. A ) -> NN0 C_ CC )
50		fss	|- ( ( a : ( 1 ... K ) --> NN0 /\ NN0 C_ CC ) -> a : ( 1 ... K ) --> CC )
51	20 49 50	syl2anc	|- ( ( ph /\ a e. A ) -> a : ( 1 ... K ) --> CC )
52	51	ffvelrnda	|- ( ( ( ph /\ a e. A ) /\ n e. ( 1 ... K ) ) -> ( a ` n ) e. CC )
53	38 45 46 47 52	fsumf1o	|- ( ( ph /\ a e. A ) -> sum_ n e. ( 1 ... K ) ( a ` n ) = sum_ i e. S ( a ` ( `' Z ` i ) ) )
54	53	eqcomd	|- ( ( ph /\ a e. A ) -> sum_ i e. S ( a ` ( `' Z ` i ) ) = sum_ n e. ( 1 ... K ) ( a ` n ) )
55		fveq2	|- ( n = i -> ( a ` n ) = ( a ` i ) )
56	55	cbvsumv	|- sum_ n e. ( 1 ... K ) ( a ` n ) = sum_ i e. ( 1 ... K ) ( a ` i )
57	56	a1i	|- ( ( ph /\ a e. A ) -> sum_ n e. ( 1 ... K ) ( a ` n ) = sum_ i e. ( 1 ... K ) ( a ` i ) )
58	19	simprd	|- ( ( ph /\ a e. A ) -> sum_ i e. ( 1 ... K ) ( a ` i ) = N )
59	57 58	eqtrd	|- ( ( ph /\ a e. A ) -> sum_ n e. ( 1 ... K ) ( a ` n ) = N )
60	54 59	eqtrd	|- ( ( ph /\ a e. A ) -> sum_ i e. S ( a ` ( `' Z ` i ) ) = N )
61	37 60	eqtrd	|- ( ( ph /\ a e. A ) -> sum_ i e. S ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) = N )
62	29 61	jca	|- ( ( ph /\ a e. A ) -> ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) : S --> NN0 /\ sum_ i e. S ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) = N ) )
63		fzfid	|- ( ph -> ( 1 ... K ) e. Fin )
64	63	adantr	|- ( ( ph /\ a e. A ) -> ( 1 ... K ) e. Fin )
65	63 5 41	syl2anc	|- ( ph -> ( 1 ... K ) ~~ S )
66	65	ensymd	|- ( ph -> S ~~ ( 1 ... K ) )
67	66	adantr	|- ( ( ph /\ a e. A ) -> S ~~ ( 1 ... K ) )
68	64 67 44	syl2anc	|- ( ( ph /\ a e. A ) -> S e. Fin )
69	68	mptexd	|- ( ( ph /\ a e. A ) -> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) e. _V )
70		feq1	|- ( h = ( x e. S |-> ( a ` ( `' Z ` x ) ) ) -> ( h : S --> NN0 <-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) : S --> NN0 ) )
71		simpl	|- ( ( h = ( x e. S |-> ( a ` ( `' Z ` x ) ) ) /\ i e. S ) -> h = ( x e. S |-> ( a ` ( `' Z ` x ) ) ) )
72	71	fveq1d	|- ( ( h = ( x e. S |-> ( a ` ( `' Z ` x ) ) ) /\ i e. S ) -> ( h ` i ) = ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) )
73	72	sumeq2dv	|- ( h = ( x e. S |-> ( a ` ( `' Z ` x ) ) ) -> sum_ i e. S ( h ` i ) = sum_ i e. S ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) )
74	73	eqeq1d	|- ( h = ( x e. S |-> ( a ` ( `' Z ` x ) ) ) -> ( sum_ i e. S ( h ` i ) = N <-> sum_ i e. S ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) = N ) )
75	70 74	anbi12d	|- ( h = ( x e. S |-> ( a ` ( `' Z ` x ) ) ) -> ( ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) <-> ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) : S --> NN0 /\ sum_ i e. S ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) = N ) ) )
76	75	elabg	|- ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) e. _V -> ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) e. { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } <-> ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) : S --> NN0 /\ sum_ i e. S ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) = N ) ) )
77	69 76	syl	|- ( ( ph /\ a e. A ) -> ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) e. { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } <-> ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) : S --> NN0 /\ sum_ i e. S ( ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ` i ) = N ) ) )
78	62 77	mpbird	|- ( ( ph /\ a e. A ) -> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) e. { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } )
79	4	a1i	|- ( ( ph /\ a e. A ) -> B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } )
80	78 79	eleqtrrd	|- ( ( ph /\ a e. A ) -> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) e. B )
81	80 6	fmptd	|- ( ph -> F : A --> B )