sticksstones18

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

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

Proof

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

Metamath Proof Explorer

Theorem sticksstones18

Proof