sticksstones19

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

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

Proof

Step	Hyp	Ref	Expression
1		sticksstones19.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones19.2	$⊢ φ \to K \in ℕ_{0}$
3		sticksstones19.3	$⊢ A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
4		sticksstones19.4	$⊢ B = \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\}$
5		sticksstones19.5	$⊢ φ \to Z : (1 \dots K) \underset{1-1 onto}{⟶} S$
6		sticksstones19.6	$⊢ F = (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x))))$
7		sticksstones19.7	$⊢ G = (b \in B ⟼ (y \in (1 \dots K) ⟼ b (Z (y))))$
8	1 2 3 4 5 6	sticksstones18	$⊢ φ \to F : A ⟶ B$
9	1 2 3 4 5 7	sticksstones17	$⊢ φ \to G : B ⟶ A$
10	7	a1i	$⊢ (φ \land c \in A) \to G = (b \in B ⟼ (y \in (1 \dots K) ⟼ b (Z (y))))$
11		simplr	$⊢ (((φ \land c \in A) \land b = F (c)) \land y \in (1 \dots K)) \to b = F (c)$
12	11	fveq1d	$⊢ (((φ \land c \in A) \land b = F (c)) \land y \in (1 \dots K)) \to b (Z (y)) = F (c) (Z (y))$
13	12	mpteq2dva	$⊢ ((φ \land c \in A) \land b = F (c)) \to (y \in (1 \dots K) ⟼ b (Z (y))) = (y \in (1 \dots K) ⟼ F (c) (Z (y)))$
14	8	ffvelcdmda	$⊢ (φ \land c \in A) \to F (c) \in B$
15		fzfid	$⊢ (φ \land c \in A) \to (1 \dots K) \in Fin$
16	15	mptexd	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ F (c) (Z (y))) \in V$
17	10 13 14 16	fvmptd	$⊢ (φ \land c \in A) \to G (F (c)) = (y \in (1 \dots K) ⟼ F (c) (Z (y)))$
18	6	a1i	$⊢ (φ \land c \in A \land y \in (1 \dots K)) \to F = (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x))))$
19	18	fveq1d	$⊢ (φ \land c \in A \land y \in (1 \dots K)) \to F (c) = (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) (c)$
20	19	fveq1d	$⊢ (φ \land c \in A \land y \in (1 \dots K)) \to F (c) (Z (y)) = (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) (c) (Z (y))$
21	20	3expa	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to F (c) (Z (y)) = (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) (c) (Z (y))$
22	21	mpteq2dva	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ F (c) (Z (y))) = (y \in (1 \dots K) ⟼ (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) (c) (Z (y)))$
23		eqidd	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) = (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x))))$
24		simplr	$⊢ ((((φ \land c \in A) \land y \in (1 \dots K)) \land a = c) \land x \in S) \to a = c$
25	24	fveq1d	$⊢ ((((φ \land c \in A) \land y \in (1 \dots K)) \land a = c) \land x \in S) \to a (Z^{-1} (x)) = c (Z^{-1} (x))$
26	25	mpteq2dva	$⊢ (((φ \land c \in A) \land y \in (1 \dots K)) \land a = c) \to (x \in S ⟼ a (Z^{-1} (x))) = (x \in S ⟼ c (Z^{-1} (x)))$
27		simplr	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to c \in A$
28		fzfid	$⊢ φ \to (1 \dots K) \in Fin$
29		f1oenfi	$⊢ ((1 \dots K) \in Fin \land Z : (1 \dots K) \underset{1-1 onto}{⟶} S) \to (1 \dots K) \approx S$
30	28 5 29	syl2anc	$⊢ φ \to (1 \dots K) \approx S$
31	30	ensymd	$⊢ φ \to S \approx (1 \dots K)$
32		enfii	$⊢ ((1 \dots K) \in Fin \land S \approx (1 \dots K)) \to S \in Fin$
33	28 31 32	syl2anc	$⊢ φ \to S \in Fin$
34	33	adantr	$⊢ (φ \land c \in A) \to S \in Fin$
35	34	adantr	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to S \in Fin$
36	35	mptexd	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to (x \in S ⟼ c (Z^{-1} (x))) \in V$
37	23 26 27 36	fvmptd	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) (c) = (x \in S ⟼ c (Z^{-1} (x)))$
38	37	fveq1d	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) (c) (Z (y)) = (x \in S ⟼ c (Z^{-1} (x))) (Z (y))$
39	38	mpteq2dva	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) (c) (Z (y))) = (y \in (1 \dots K) ⟼ (x \in S ⟼ c (Z^{-1} (x))) (Z (y)))$
40		eqidd	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to (x \in S ⟼ c (Z^{-1} (x))) = (x \in S ⟼ c (Z^{-1} (x)))$
41		simpr	$⊢ (((φ \land c \in A) \land y \in (1 \dots K)) \land x = Z (y)) \to x = Z (y)$
42	41	fveq2d	$⊢ (((φ \land c \in A) \land y \in (1 \dots K)) \land x = Z (y)) \to Z^{-1} (x) = Z^{-1} (Z (y))$
43	42	fveq2d	$⊢ (((φ \land c \in A) \land y \in (1 \dots K)) \land x = Z (y)) \to c (Z^{-1} (x)) = c (Z^{-1} (Z (y)))$
44		f1of	$⊢ Z : (1 \dots K) \underset{1-1 onto}{⟶} S \to Z : (1 \dots K) ⟶ S$
45	5 44	syl	$⊢ φ \to Z : (1 \dots K) ⟶ S$
46	45	adantr	$⊢ (φ \land c \in A) \to Z : (1 \dots K) ⟶ S$
47	46	ffvelcdmda	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to Z (y) \in S$
48		fvexd	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to c (Z^{-1} (Z (y))) \in V$
49	40 43 47 48	fvmptd	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to (x \in S ⟼ c (Z^{-1} (x))) (Z (y)) = c (Z^{-1} (Z (y)))$
50	49	mpteq2dva	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ (x \in S ⟼ c (Z^{-1} (x))) (Z (y))) = (y \in (1 \dots K) ⟼ c (Z^{-1} (Z (y))))$
51	5	ad2antrr	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to Z : (1 \dots K) \underset{1-1 onto}{⟶} S$
52		simpr	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to y \in (1 \dots K)$
53		f1ocnvfv1	$⊢ (Z : (1 \dots K) \underset{1-1 onto}{⟶} S \land y \in (1 \dots K)) \to Z^{-1} (Z (y)) = y$
54	51 52 53	syl2anc	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to Z^{-1} (Z (y)) = y$
55	54	fveq2d	$⊢ ((φ \land c \in A) \land y \in (1 \dots K)) \to c (Z^{-1} (Z (y))) = c (y)$
56	55	mpteq2dva	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ c (Z^{-1} (Z (y)))) = (y \in (1 \dots K) ⟼ c (y))$
57		simpr	$⊢ (φ \land c \in A) \to c \in A$
58	3	a1i	$⊢ (φ \land c \in A) \to A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
59	57 58	eleqtrd	$⊢ (φ \land c \in A) \to c \in \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
60		vex	$⊢ c \in V$
61		feq1	$⊢ g = c \to (g : (1 \dots K) ⟶ ℕ_{0} \leftrightarrow c : (1 \dots K) ⟶ ℕ_{0})$
62		simpl	$⊢ (g = c \land i \in (1 \dots K)) \to g = c$
63	62	fveq1d	$⊢ (g = c \land i \in (1 \dots K)) \to g (i) = c (i)$
64	63	sumeq2dv	$⊢ g = c \to \sum_{i = 1}^{K} g (i) = \sum_{i = 1}^{K} c (i)$
65	64	eqeq1d	$⊢ g = c \to (\sum_{i = 1}^{K} g (i) = N \leftrightarrow \sum_{i = 1}^{K} c (i) = N)$
66	61 65	anbi12d	$⊢ g = c \to ((g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N) \leftrightarrow (c : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} c (i) = N))$
67	60 66	elab	$⊢ c \in \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\} \leftrightarrow (c : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} c (i) = N)$
68	59 67	sylib	$⊢ (φ \land c \in A) \to (c : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} c (i) = N)$
69	68	simpld	$⊢ (φ \land c \in A) \to c : (1 \dots K) ⟶ ℕ_{0}$
70		ffn	$⊢ c : (1 \dots K) ⟶ ℕ_{0} \to c Fn (1 \dots K)$
71	69 70	syl	$⊢ (φ \land c \in A) \to c Fn (1 \dots K)$
72		dffn5	$⊢ c Fn (1 \dots K) \leftrightarrow c = (y \in (1 \dots K) ⟼ c (y))$
73	71 72	sylib	$⊢ (φ \land c \in A) \to c = (y \in (1 \dots K) ⟼ c (y))$
74	73	eqcomd	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ c (y)) = c$
75	56 74	eqtrd	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ c (Z^{-1} (Z (y)))) = c$
76	50 75	eqtrd	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ (x \in S ⟼ c (Z^{-1} (x))) (Z (y))) = c$
77	39 76	eqtrd	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x)))) (c) (Z (y))) = c$
78	22 77	eqtrd	$⊢ (φ \land c \in A) \to (y \in (1 \dots K) ⟼ F (c) (Z (y))) = c$
79	17 78	eqtrd	$⊢ (φ \land c \in A) \to G (F (c)) = c$
80	79	ralrimiva	$⊢ φ \to \forall c \in A G (F (c)) = c$
81	6	a1i	$⊢ (φ \land d \in B) \to F = (a \in A ⟼ (x \in S ⟼ a (Z^{-1} (x))))$
82		simplr	$⊢ (((φ \land d \in B) \land a = G (d)) \land x \in S) \to a = G (d)$
83	82	fveq1d	$⊢ (((φ \land d \in B) \land a = G (d)) \land x \in S) \to a (Z^{-1} (x)) = G (d) (Z^{-1} (x))$
84	83	mpteq2dva	$⊢ ((φ \land d \in B) \land a = G (d)) \to (x \in S ⟼ a (Z^{-1} (x))) = (x \in S ⟼ G (d) (Z^{-1} (x)))$
85	9	ffvelcdmda	$⊢ (φ \land d \in B) \to G (d) \in A$
86	33	adantr	$⊢ (φ \land d \in B) \to S \in Fin$
87	86	mptexd	$⊢ (φ \land d \in B) \to (x \in S ⟼ G (d) (Z^{-1} (x))) \in V$
88	81 84 85 87	fvmptd	$⊢ (φ \land d \in B) \to F (G (d)) = (x \in S ⟼ G (d) (Z^{-1} (x)))$
89	7	a1i	$⊢ ((φ \land d \in B) \land x \in S) \to G = (b \in B ⟼ (y \in (1 \dots K) ⟼ b (Z (y))))$
90		simplr	$⊢ ((((φ \land d \in B) \land x \in S) \land b = d) \land y \in (1 \dots K)) \to b = d$
91	90	fveq1d	$⊢ ((((φ \land d \in B) \land x \in S) \land b = d) \land y \in (1 \dots K)) \to b (Z (y)) = d (Z (y))$
92	91	mpteq2dva	$⊢ (((φ \land d \in B) \land x \in S) \land b = d) \to (y \in (1 \dots K) ⟼ b (Z (y))) = (y \in (1 \dots K) ⟼ d (Z (y)))$
93		simplr	$⊢ ((φ \land d \in B) \land x \in S) \to d \in B$
94		fzfid	$⊢ ((φ \land d \in B) \land x \in S) \to (1 \dots K) \in Fin$
95	94	mptexd	$⊢ ((φ \land d \in B) \land x \in S) \to (y \in (1 \dots K) ⟼ d (Z (y))) \in V$
96	89 92 93 95	fvmptd	$⊢ ((φ \land d \in B) \land x \in S) \to G (d) = (y \in (1 \dots K) ⟼ d (Z (y)))$
97	96	fveq1d	$⊢ ((φ \land d \in B) \land x \in S) \to G (d) (Z^{-1} (x)) = (y \in (1 \dots K) ⟼ d (Z (y))) (Z^{-1} (x))$
98	97	mpteq2dva	$⊢ (φ \land d \in B) \to (x \in S ⟼ G (d) (Z^{-1} (x))) = (x \in S ⟼ (y \in (1 \dots K) ⟼ d (Z (y))) (Z^{-1} (x)))$
99		eqidd	$⊢ ((φ \land d \in B) \land x \in S) \to (y \in (1 \dots K) ⟼ d (Z (y))) = (y \in (1 \dots K) ⟼ d (Z (y)))$
100		simpr	$⊢ (((φ \land d \in B) \land x \in S) \land y = Z^{-1} (x)) \to y = Z^{-1} (x)$
101	100	fveq2d	$⊢ (((φ \land d \in B) \land x \in S) \land y = Z^{-1} (x)) \to Z (y) = Z (Z^{-1} (x))$
102	101	fveq2d	$⊢ (((φ \land d \in B) \land x \in S) \land y = Z^{-1} (x)) \to d (Z (y)) = d (Z (Z^{-1} (x)))$
103		f1ocnv	$⊢ Z : (1 \dots K) \underset{1-1 onto}{⟶} S \to Z^{-1} : S \underset{1-1 onto}{⟶} (1 \dots K)$
104	5 103	syl	$⊢ φ \to Z^{-1} : S \underset{1-1 onto}{⟶} (1 \dots K)$
105		f1of	$⊢ Z^{-1} : S \underset{1-1 onto}{⟶} (1 \dots K) \to Z^{-1} : S ⟶ (1 \dots K)$
106	104 105	syl	$⊢ φ \to Z^{-1} : S ⟶ (1 \dots K)$
107	106	adantr	$⊢ (φ \land d \in B) \to Z^{-1} : S ⟶ (1 \dots K)$
108	107	ffvelcdmda	$⊢ ((φ \land d \in B) \land x \in S) \to Z^{-1} (x) \in (1 \dots K)$
109		fvexd	$⊢ ((φ \land d \in B) \land x \in S) \to d (Z (Z^{-1} (x))) \in V$
110	99 102 108 109	fvmptd	$⊢ ((φ \land d \in B) \land x \in S) \to (y \in (1 \dots K) ⟼ d (Z (y))) (Z^{-1} (x)) = d (Z (Z^{-1} (x)))$
111	110	mpteq2dva	$⊢ (φ \land d \in B) \to (x \in S ⟼ (y \in (1 \dots K) ⟼ d (Z (y))) (Z^{-1} (x))) = (x \in S ⟼ d (Z (Z^{-1} (x))))$
112	5	ad2antrr	$⊢ ((φ \land d \in B) \land x \in S) \to Z : (1 \dots K) \underset{1-1 onto}{⟶} S$
113		simpr	$⊢ ((φ \land d \in B) \land x \in S) \to x \in S$
114		f1ocnvfv2	$⊢ (Z : (1 \dots K) \underset{1-1 onto}{⟶} S \land x \in S) \to Z (Z^{-1} (x)) = x$
115	112 113 114	syl2anc	$⊢ ((φ \land d \in B) \land x \in S) \to Z (Z^{-1} (x)) = x$
116	115	fveq2d	$⊢ ((φ \land d \in B) \land x \in S) \to d (Z (Z^{-1} (x))) = d (x)$
117	116	mpteq2dva	$⊢ (φ \land d \in B) \to (x \in S ⟼ d (Z (Z^{-1} (x)))) = (x \in S ⟼ d (x))$
118		simpr	$⊢ (φ \land d \in B) \to d \in B$
119	4	a1i	$⊢ (φ \land d \in B) \to B = \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\}$
120	118 119	eleqtrd	$⊢ (φ \land d \in B) \to d \in \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\}$
121		vex	$⊢ d \in V$
122		feq1	$⊢ h = d \to (h : S ⟶ ℕ_{0} \leftrightarrow d : S ⟶ ℕ_{0})$
123		simpl	$⊢ (h = d \land i \in S) \to h = d$
124	123	fveq1d	$⊢ (h = d \land i \in S) \to h (i) = d (i)$
125	124	sumeq2dv	$⊢ h = d \to \sum_{i \in S} h (i) = \sum_{i \in S} d (i)$
126	125	eqeq1d	$⊢ h = d \to (\sum_{i \in S} h (i) = N \leftrightarrow \sum_{i \in S} d (i) = N)$
127	122 126	anbi12d	$⊢ h = d \to ((h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N) \leftrightarrow (d : S ⟶ ℕ_{0} \land \sum_{i \in S} d (i) = N))$
128	121 127	elab	$⊢ d \in \{h \| (h : S ⟶ ℕ_{0} \land \sum_{i \in S} h (i) = N)\} \leftrightarrow (d : S ⟶ ℕ_{0} \land \sum_{i \in S} d (i) = N)$
129	120 128	sylib	$⊢ (φ \land d \in B) \to (d : S ⟶ ℕ_{0} \land \sum_{i \in S} d (i) = N)$
130	129	simpld	$⊢ (φ \land d \in B) \to d : S ⟶ ℕ_{0}$
131		ffn	$⊢ d : S ⟶ ℕ_{0} \to d Fn S$
132	130 131	syl	$⊢ (φ \land d \in B) \to d Fn S$
133		dffn5	$⊢ d Fn S \leftrightarrow d = (x \in S ⟼ d (x))$
134	132 133	sylib	$⊢ (φ \land d \in B) \to d = (x \in S ⟼ d (x))$
135	134	eqcomd	$⊢ (φ \land d \in B) \to (x \in S ⟼ d (x)) = d$
136	117 135	eqtrd	$⊢ (φ \land d \in B) \to (x \in S ⟼ d (Z (Z^{-1} (x)))) = d$
137	111 136	eqtrd	$⊢ (φ \land d \in B) \to (x \in S ⟼ (y \in (1 \dots K) ⟼ d (Z (y))) (Z^{-1} (x))) = d$
138	98 137	eqtrd	$⊢ (φ \land d \in B) \to (x \in S ⟼ G (d) (Z^{-1} (x))) = d$
139	88 138	eqtrd	$⊢ (φ \land d \in B) \to F (G (d)) = d$
140	139	ralrimiva	$⊢ φ \to \forall d \in B F (G (d)) = d$
141	8 9 80 140	2fvidf1od	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem sticksstones19

Proof