sticksstones17

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

	Ref	Expression
Hypotheses	sticksstones17.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones17.2	$⊢ φ \to K \in ℕ_{0}$
	sticksstones17.3	$⊢ A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
	sticksstones17.4	$⊢ B = \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\}$
	sticksstones17.5	$⊢ φ \to Z : (1 \dots K) \underset{1-1 onto}{⟶} S$
	sticksstones17.6	$⊢ G = (b \in B ⟼ (y \in (1 \dots K) ⟼ b (Z (y))))$
Assertion	sticksstones17	$⊢ φ \to G : B ⟶ A$

Proof

Step	Hyp	Ref	Expression
1		sticksstones17.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones17.2	$⊢ φ \to K \in ℕ_{0}$
3		sticksstones17.3	$⊢ A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
4		sticksstones17.4	$⊢ B = \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\}$
5		sticksstones17.5	$⊢ φ \to Z : (1 \dots K) \underset{1-1 onto}{⟶} S$
6		sticksstones17.6	$⊢ G = (b \in B ⟼ (y \in (1 \dots K) ⟼ b (Z (y))))$
7	4	eqimssi	$⊢ B \subseteq \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\}$
8	7	a1i	$⊢ φ \to B \subseteq \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\}$
9	8	sseld	$⊢ φ \to (b \in B \to b \in \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\})$
10	9	imp	$⊢ (φ \land b \in B) \to b \in \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\}$
11		vex	$⊢ b \in V$
12		feq1	$⊢ h = b \to (h : S ⟶ ℕ_{0} \leftrightarrow b : S ⟶ ℕ_{0})$
13		simpl	$⊢ (h = b \land i \in S) \to h = b$
14	13	fveq1d	$⊢ (h = b \land i \in S) \to h (i) = b (i)$
15	14	sumeq2dv	$⊢ h = b \to \sum_{i \in S} h (i) = \sum_{i \in S} b (i)$
16	15	eqeq1d	$⊢ h = b \to (\sum_{i \in S} h (i) = N \leftrightarrow \sum_{i \in S} b (i) = N)$
17	12 16	anbi12d	$⊢ h = b \to ((h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N) \leftrightarrow (b : S ⟶ ℕ_{0} \land \sum_{i \in S} b (i) = N))$
18	11 17	elab	$⊢ b \in \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\} \leftrightarrow (b : S ⟶ ℕ_{0} \land \sum_{i \in S} b (i) = N)$
19	10 18	sylib	$⊢ (φ \land b \in B) \to (b : S ⟶ ℕ_{0} \land \sum_{i \in S} b (i) = N)$
20	19	simpld	$⊢ (φ \land b \in B) \to b : S ⟶ ℕ_{0}$
21	20	adantr	$⊢ ((φ \land b \in B) \land y \in (1 \dots K)) \to b : S ⟶ ℕ_{0}$
22	21	3impa	$⊢ (φ \land b \in B \land y \in (1 \dots K)) \to b : S ⟶ ℕ_{0}$
23		f1of	$⊢ Z : (1 \dots K) \underset{1-1 onto}{⟶} S \to Z : (1 \dots K) ⟶ S$
24	5 23	syl	$⊢ φ \to Z : (1 \dots K) ⟶ S$
25	24	adantr	$⊢ (φ \land b \in B) \to Z : (1 \dots K) ⟶ S$
26	25	adantr	$⊢ ((φ \land b \in B) \land y \in (1 \dots K)) \to Z : (1 \dots K) ⟶ S$
27	26	3impa	$⊢ (φ \land b \in B \land y \in (1 \dots K)) \to Z : (1 \dots K) ⟶ S$
28		simp3	$⊢ (φ \land b \in B \land y \in (1 \dots K)) \to y \in (1 \dots K)$
29	27 28	ffvelrnd	$⊢ (φ \land b \in B \land y \in (1 \dots K)) \to Z (y) \in S$
30	22 29	ffvelrnd	$⊢ (φ \land b \in B \land y \in (1 \dots K)) \to b (Z (y)) \in ℕ_{0}$
31	30	3expa	$⊢ ((φ \land b \in B) \land y \in (1 \dots K)) \to b (Z (y)) \in ℕ_{0}$
32	31	fmpttd	$⊢ (φ \land b \in B) \to (y \in (1 \dots K) ⟼ b (Z (y))) : (1 \dots K) ⟶ ℕ_{0}$
33		eqidd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to (y \in (1 \dots K) ⟼ b (Z (y))) = (y \in (1 \dots K) ⟼ b (Z (y)))$
34		simpr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land y = i) \to y = i$
35	34	fveq2d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land y = i) \to Z (y) = Z (i)$
36	35	fveq2d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land y = i) \to b (Z (y)) = b (Z (i))$
37		simpr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \in (1 \dots K)$
38		fvexd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to b (Z (i)) \in V$
39	33 36 37 38	fvmptd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to (y \in (1 \dots K) ⟼ b (Z (y))) (i) = b (Z (i))$
40	39	sumeq2dv	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (y \in (1 \dots K) ⟼ b (Z (y))) (i) = \sum_{i = 1}^{K} b (Z (i))$
41		fveq2	$⊢ s = Z (i) \to b (s) = b (Z (i))$
42		fzfi	$⊢ (1 \dots K) \in Fin$
43	42	a1i	$⊢ (φ \land b \in B) \to (1 \dots K) \in Fin$
44	5	adantr	$⊢ (φ \land b \in B) \to Z : (1 \dots K) \underset{1-1 onto}{⟶} S$
45		eqidd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to Z (i) = Z (i)$
46		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
47	46	a1i	$⊢ (φ \land b \in B) \to ℕ_{0} \subseteq ℂ$
48		fss	$⊢ (b : S ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℂ) \to b : S ⟶ ℂ$
49	20 47 48	syl2anc	$⊢ (φ \land b \in B) \to b : S ⟶ ℂ$
50	49	ffvelrnda	$⊢ ((φ \land b \in B) \land s \in S) \to b (s) \in ℂ$
51	41 43 44 45 50	fsumf1o	$⊢ (φ \land b \in B) \to \sum_{s \in S} b (s) = \sum_{i = 1}^{K} b (Z (i))$
52	51	eqcomd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} b (Z (i)) = \sum_{s \in S} b (s)$
53		fveq2	$⊢ s = i \to b (s) = b (i)$
54	53	cbvsumv	$⊢ \sum_{s \in S} b (s) = \sum_{i \in S} b (i)$
55	54	a1i	$⊢ (φ \land b \in B) \to \sum_{s \in S} b (s) = \sum_{i \in S} b (i)$
56	19	simprd	$⊢ (φ \land b \in B) \to \sum_{i \in S} b (i) = N$
57	55 56	eqtrd	$⊢ (φ \land b \in B) \to \sum_{s \in S} b (s) = N$
58	52 57	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} b (Z (i)) = N$
59	40 58	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (y \in (1 \dots K) ⟼ b (Z (y))) (i) = N$
60	32 59	jca	$⊢ (φ \land b \in B) \to ((y \in (1 \dots K) ⟼ b (Z (y))) : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} (y \in (1 \dots K) ⟼ b (Z (y))) (i) = N)$
61		fzfid	$⊢ (φ \land b \in B) \to (1 \dots K) \in Fin$
62	61	mptexd	$⊢ (φ \land b \in B) \to (y \in (1 \dots K) ⟼ b (Z (y))) \in V$
63		feq1	$⊢ g = (y \in (1 \dots K) ⟼ b (Z (y))) \to (g : (1 \dots K) ⟶ ℕ_{0} \leftrightarrow (y \in (1 \dots K) ⟼ b (Z (y))) : (1 \dots K) ⟶ ℕ_{0})$
64		simpl	$⊢ (g = (y \in (1 \dots K) ⟼ b (Z (y))) \land i \in (1 \dots K)) \to g = (y \in (1 \dots K) ⟼ b (Z (y)))$
65	64	fveq1d	$⊢ (g = (y \in (1 \dots K) ⟼ b (Z (y))) \land i \in (1 \dots K)) \to g (i) = (y \in (1 \dots K) ⟼ b (Z (y))) (i)$
66	65	sumeq2dv	$⊢ g = (y \in (1 \dots K) ⟼ b (Z (y))) \to \sum_{i = 1}^{K} g (i) = \sum_{i = 1}^{K} (y \in (1 \dots K) ⟼ b (Z (y))) (i)$
67	66	eqeq1d	$⊢ g = (y \in (1 \dots K) ⟼ b (Z (y))) \to (\sum_{i = 1}^{K} g (i) = N \leftrightarrow \sum_{i = 1}^{K} (y \in (1 \dots K) ⟼ b (Z (y))) (i) = N)$
68	63 67	anbi12d	$⊢ g = (y \in (1 \dots K) ⟼ b (Z (y))) \to ((g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N) \leftrightarrow ((y \in (1 \dots K) ⟼ b (Z (y))) : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} (y \in (1 \dots K) ⟼ b (Z (y))) (i) = N))$
69	68	elabg	$⊢ (y \in (1 \dots K) ⟼ b (Z (y))) \in V \to ((y \in (1 \dots K) ⟼ b (Z (y))) \in \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\} \leftrightarrow ((y \in (1 \dots K) ⟼ b (Z (y))) : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} (y \in (1 \dots K) ⟼ b (Z (y))) (i) = N))$
70	62 69	syl	$⊢ (φ \land b \in B) \to ((y \in (1 \dots K) ⟼ b (Z (y))) \in \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\} \leftrightarrow ((y \in (1 \dots K) ⟼ b (Z (y))) : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} (y \in (1 \dots K) ⟼ b (Z (y))) (i) = N))$
71	60 70	mpbird	$⊢ (φ \land b \in B) \to (y \in (1 \dots K) ⟼ b (Z (y))) \in \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
72	3	a1i	$⊢ (φ \land b \in B) \to A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
73	71 72	eleqtrrd	$⊢ (φ \land b \in B) \to (y \in (1 \dots K) ⟼ b (Z (y))) \in A$
74	73 6	fmptd	$⊢ φ \to G : B ⟶ A$

Metamath Proof Explorer

Theorem sticksstones17

Proof