sticksstones11

Description: Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones11.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones11.2	$⊢ φ \to K = 0$
	sticksstones11.3	$⊢ F = (a \in A ⟼ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)))$
	sticksstones11.4	$⊢ G = (b \in B ⟼ if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))))$
	sticksstones11.5	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
	sticksstones11.6	$⊢ B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
Assertion	sticksstones11	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		sticksstones11.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones11.2	$⊢ φ \to K = 0$
3		sticksstones11.3	$⊢ F = (a \in A ⟼ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)))$
4		sticksstones11.4	$⊢ G = (b \in B ⟼ if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))))$
5		sticksstones11.5	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
6		sticksstones11.6	$⊢ B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
7		0nn0	$⊢ 0 \in ℕ_{0}$
8	7	a1i	$⊢ φ \to 0 \in ℕ_{0}$
9	2 8	eqeltrd	$⊢ φ \to K \in ℕ_{0}$
10	1 9 3 5 6	sticksstones8	$⊢ φ \to F : A ⟶ B$
11	1 2 4 5 6	sticksstones9	$⊢ φ \to G : B ⟶ A$
12	5	a1i	$⊢ φ \to A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
13		nfv	$⊢ Ⅎ u φ$
14		nfcv	$⊢ \underline{Ⅎ} u \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
15		nfcv	$⊢ \underline{Ⅎ} u \{\{⟨1, N⟩\}\}$
16		ffn	$⊢ u : \{1\} ⟶ ℕ_{0} \to u Fn \{1\}$
17	16	ad2antrl	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u Fn \{1\}$
18		1nn	$⊢ 1 \in ℕ$
19	18	a1i	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to 1 \in ℕ$
20	1	adantr	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to N \in ℕ_{0}$
21		fnsng	$⊢ (1 \in ℕ \land N \in ℕ_{0}) \to \{⟨1, N⟩\} Fn \{1\}$
22	19 20 21	syl2anc	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to \{⟨1, N⟩\} Fn \{1\}$
23		elsni	$⊢ p \in \{1\} \to p = 1$
24	23	adantl	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \to p = 1$
25		simpr	$⊢ (((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \land p = 1) \to p = 1$
26	25	fveq2d	$⊢ (((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \land p = 1) \to u (p) = u (1)$
27		simprl	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u : \{1\} ⟶ ℕ_{0}$
28		1ex	$⊢ 1 \in V$
29	28	snid	$⊢ 1 \in \{1\}$
30	29	a1i	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to 1 \in \{1\}$
31	27 30	ffvelcdmd	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u (1) \in ℕ_{0}$
32	31	nn0cnd	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u (1) \in ℂ$
33		fveq2	$⊢ i = 1 \to u (i) = u (1)$
34	33	sumsn	$⊢ (1 \in ℕ \land u (1) \in ℂ) \to \sum_{i \in \{1\}} u (i) = u (1)$
35	19 32 34	syl2anc	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to \sum_{i \in \{1\}} u (i) = u (1)$
36	35	adantr	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land \sum_{i \in \{1\}} u (i) = u (1)) \to \sum_{i \in \{1\}} u (i) = u (1)$
37	36	eqcomd	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land \sum_{i \in \{1\}} u (i) = u (1)) \to u (1) = \sum_{i \in \{1\}} u (i)$
38		simplrr	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land \sum_{i \in \{1\}} u (i) = u (1)) \to \sum_{i \in \{1\}} u (i) = N$
39	37 38	eqtrd	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land \sum_{i \in \{1\}} u (i) = u (1)) \to u (1) = N$
40	39	ex	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to (\sum_{i \in \{1\}} u (i) = u (1) \to u (1) = N)$
41	35 40	mpd	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u (1) = N$
42	41	adantr	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \to u (1) = N$
43	18	a1i	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \to 1 \in ℕ$
44	20	adantr	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \to N \in ℕ_{0}$
45		fvsng	$⊢ (1 \in ℕ \land N \in ℕ_{0}) \to \{⟨1, N⟩\} (1) = N$
46	43 44 45	syl2anc	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \to \{⟨1, N⟩\} (1) = N$
47	46	eqcomd	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \to N = \{⟨1, N⟩\} (1)$
48	42 47	eqtrd	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \to u (1) = \{⟨1, N⟩\} (1)$
49	48	adantr	$⊢ (((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \land p = 1) \to u (1) = \{⟨1, N⟩\} (1)$
50	25	eqcomd	$⊢ (((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \land p = 1) \to 1 = p$
51	50	fveq2d	$⊢ (((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \land p = 1) \to \{⟨1, N⟩\} (1) = \{⟨1, N⟩\} (p)$
52	26 49 51	3eqtrd	$⊢ (((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \land p = 1) \to u (p) = \{⟨1, N⟩\} (p)$
53	24 52	mpdan	$⊢ ((φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \land p \in \{1\}) \to u (p) = \{⟨1, N⟩\} (p)$
54	17 22 53	eqfnfvd	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u = \{⟨1, N⟩\}$
55		fsng	$⊢ (1 \in ℕ \land N \in ℕ_{0}) \to (u : \{1\} ⟶ \{N\} \leftrightarrow u = \{⟨1, N⟩\})$
56	19 20 55	syl2anc	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to (u : \{1\} ⟶ \{N\} \leftrightarrow u = \{⟨1, N⟩\})$
57	54 56	mpbird	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u : \{1\} ⟶ \{N\}$
58		ssidd	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to \{N\} \subseteq \{N\}$
59		fss	$⊢ (u : \{1\} ⟶ \{N\} \land \{N\} \subseteq \{N\}) \to u : \{1\} ⟶ \{N\}$
60	57 58 59	syl2anc	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u : \{1\} ⟶ \{N\}$
61	60 58 59	syl2anc	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u : \{1\} ⟶ \{N\}$
62	61 56	mpbid	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u = \{⟨1, N⟩\}$
63		vex	$⊢ u \in V$
64	63	elsn	$⊢ u \in \{\{⟨1, N⟩\}\} \leftrightarrow u = \{⟨1, N⟩\}$
65	62 64	sylibr	$⊢ (φ \land (u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N)) \to u \in \{\{⟨1, N⟩\}\}$
66	65	ex	$⊢ φ \to ((u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N) \to u \in \{\{⟨1, N⟩\}\})$
67		1zzd	$⊢ φ \to 1 \in ℤ$
68		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
69	67 68	syl	$⊢ φ \to (1 \dots 1) = \{1\}$
70	69	eqcomd	$⊢ φ \to \{1\} = (1 \dots 1)$
71		1e0p1	$⊢ 1 = 0 + 1$
72	71	a1i	$⊢ φ \to 1 = 0 + 1$
73	72	oveq2d	$⊢ φ \to (1 \dots 1) = (1 \dots 0 + 1)$
74	70 73	eqtrd	$⊢ φ \to \{1\} = (1 \dots 0 + 1)$
75	2	eqcomd	$⊢ φ \to 0 = K$
76	75	oveq1d	$⊢ φ \to 0 + 1 = K + 1$
77	76	oveq2d	$⊢ φ \to (1 \dots 0 + 1) = (1 \dots K + 1)$
78	74 77	eqtrd	$⊢ φ \to \{1\} = (1 \dots K + 1)$
79	78	feq2d	$⊢ φ \to (u : \{1\} ⟶ ℕ_{0} \leftrightarrow u : (1 \dots K + 1) ⟶ ℕ_{0})$
80	78	sumeq1d	$⊢ φ \to \sum_{i \in \{1\}} u (i) = \sum_{i = 1}^{K + 1} u (i)$
81	80	eqeq1d	$⊢ φ \to (\sum_{i \in \{1\}} u (i) = N \leftrightarrow \sum_{i = 1}^{K + 1} u (i) = N)$
82	79 81	anbi12d	$⊢ φ \to ((u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N) \leftrightarrow (u : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} u (i) = N))$
83	82	imbi1d	$⊢ φ \to (((u : \{1\} ⟶ ℕ_{0} \land \sum_{i \in \{1\}} u (i) = N) \to u \in \{\{⟨1, N⟩\}\}) \leftrightarrow ((u : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} u (i) = N) \to u \in \{\{⟨1, N⟩\}\}))$
84	66 83	mpbid	$⊢ φ \to ((u : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} u (i) = N) \to u \in \{\{⟨1, N⟩\}\})$
85		feq1	$⊢ g = u \to (g : (1 \dots K + 1) ⟶ ℕ_{0} \leftrightarrow u : (1 \dots K + 1) ⟶ ℕ_{0})$
86		simpl	$⊢ (g = u \land i \in (1 \dots K + 1)) \to g = u$
87	86	fveq1d	$⊢ (g = u \land i \in (1 \dots K + 1)) \to g (i) = u (i)$
88	87	sumeq2dv	$⊢ g = u \to \sum_{i = 1}^{K + 1} g (i) = \sum_{i = 1}^{K + 1} u (i)$
89	88	eqeq1d	$⊢ g = u \to (\sum_{i = 1}^{K + 1} g (i) = N \leftrightarrow \sum_{i = 1}^{K + 1} u (i) = N)$
90	85 89	anbi12d	$⊢ g = u \to ((g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N) \leftrightarrow (u : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} u (i) = N))$
91	63 90	elab	$⊢ u \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (u : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} u (i) = N)$
92	91	a1i	$⊢ φ \to (u \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (u : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} u (i) = N))$
93	92	imbi1d	$⊢ φ \to ((u \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \to u \in \{\{⟨1, N⟩\}\}) \leftrightarrow ((u : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} u (i) = N) \to u \in \{\{⟨1, N⟩\}\}))$
94	84 93	mpbird	$⊢ φ \to (u \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \to u \in \{\{⟨1, N⟩\}\})$
95	94	imp	$⊢ (φ \land u \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}) \to u \in \{\{⟨1, N⟩\}\}$
96	95	ex	$⊢ φ \to (u \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \to u \in \{\{⟨1, N⟩\}\})$
97	13 14 15 96	ssrd	$⊢ φ \to \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \subseteq \{\{⟨1, N⟩\}\}$
98	18	a1i	$⊢ φ \to 1 \in ℕ$
99	98 1 55	syl2anc	$⊢ φ \to (u : \{1\} ⟶ \{N\} \leftrightarrow u = \{⟨1, N⟩\})$
100	99	bicomd	$⊢ φ \to (u = \{⟨1, N⟩\} \leftrightarrow u : \{1\} ⟶ \{N\})$
101	100	biimpd	$⊢ φ \to (u = \{⟨1, N⟩\} \to u : \{1\} ⟶ \{N\})$
102		elsni	$⊢ u \in \{\{⟨1, N⟩\}\} \to u = \{⟨1, N⟩\}$
103	101 102	impel	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to u : \{1\} ⟶ \{N\}$
104	1	snssd	$⊢ φ \to \{N\} \subseteq ℕ_{0}$
105	104	adantr	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to \{N\} \subseteq ℕ_{0}$
106		fss	$⊢ (u : \{1\} ⟶ \{N\} \land \{N\} \subseteq ℕ_{0}) \to u : \{1\} ⟶ ℕ_{0}$
107	103 105 106	syl2anc	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to u : \{1\} ⟶ ℕ_{0}$
108	79	adantr	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to (u : \{1\} ⟶ ℕ_{0} \leftrightarrow u : (1 \dots K + 1) ⟶ ℕ_{0})$
109	107 108	mpbid	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to u : (1 \dots K + 1) ⟶ ℕ_{0}$
110	102	adantl	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to u = \{⟨1, N⟩\}$
111	78	3ad2ant1	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to \{1\} = (1 \dots K + 1)$
112	111	eqcomd	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to (1 \dots K + 1) = \{1\}$
113	112	sumeq1d	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to \sum_{i = 1}^{K + 1} u (i) = \sum_{i \in \{1\}} u (i)$
114	18	a1i	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to 1 \in ℕ$
115	1	3ad2ant1	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to N \in ℕ_{0}$
116	115	nn0cnd	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to N \in ℂ$
117	114 115 45	syl2anc	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to \{⟨1, N⟩\} (1) = N$
118	117	eqcomd	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to N = \{⟨1, N⟩\} (1)$
119	110	3adant3	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to u = \{⟨1, N⟩\}$
120	119	fveq1d	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to u (1) = \{⟨1, N⟩\} (1)$
121	118 120	eqtr4d	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to N = u (1)$
122	121	eleq1d	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to (N \in ℂ \leftrightarrow u (1) \in ℂ)$
123	116 122	mpbid	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to u (1) \in ℂ$
124	114 123 34	syl2anc	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to \sum_{i \in \{1\}} u (i) = u (1)$
125	120 117	eqtrd	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to u (1) = N$
126	124 125	eqtrd	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to \sum_{i \in \{1\}} u (i) = N$
127	113 126	eqtrd	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\} \land u = \{⟨1, N⟩\}) \to \sum_{i = 1}^{K + 1} u (i) = N$
128	127	3expa	$⊢ ((φ \land u \in \{\{⟨1, N⟩\}\}) \land u = \{⟨1, N⟩\}) \to \sum_{i = 1}^{K + 1} u (i) = N$
129	110 128	mpdan	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to \sum_{i = 1}^{K + 1} u (i) = N$
130	109 129	jca	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to (u : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} u (i) = N)$
131	130 91	sylibr	$⊢ (φ \land u \in \{\{⟨1, N⟩\}\}) \to u \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
132	131	ex	$⊢ φ \to (u \in \{\{⟨1, N⟩\}\} \to u \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\})$
133	13 15 14 132	ssrd	$⊢ φ \to \{\{⟨1, N⟩\}\} \subseteq \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
134	97 133	eqssd	$⊢ φ \to \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} = \{\{⟨1, N⟩\}\}$
135	12 134	eqtrd	$⊢ φ \to A = \{\{⟨1, N⟩\}\}$
136		eqss	$⊢ A = \{\{⟨1, N⟩\}\} \leftrightarrow (A \subseteq \{\{⟨1, N⟩\}\} \land \{\{⟨1, N⟩\}\} \subseteq A)$
137	136	biimpi	$⊢ A = \{\{⟨1, N⟩\}\} \to (A \subseteq \{\{⟨1, N⟩\}\} \land \{\{⟨1, N⟩\}\} \subseteq A)$
138	137	simpld	$⊢ A = \{\{⟨1, N⟩\}\} \to A \subseteq \{\{⟨1, N⟩\}\}$
139	135 138	syl	$⊢ φ \to A \subseteq \{\{⟨1, N⟩\}\}$
140		fss	$⊢ (G : B ⟶ A \land A \subseteq \{\{⟨1, N⟩\}\}) \to G : B ⟶ \{\{⟨1, N⟩\}\}$
141	11 139 140	syl2anc	$⊢ φ \to G : B ⟶ \{\{⟨1, N⟩\}\}$
142	141	adantr	$⊢ (φ \land c \in A) \to G : B ⟶ \{\{⟨1, N⟩\}\}$
143	10	ffvelcdmda	$⊢ (φ \land c \in A) \to F (c) \in B$
144		fvconst	$⊢ (G : B ⟶ \{\{⟨1, N⟩\}\} \land F (c) \in B) \to G (F (c)) = \{⟨1, N⟩\}$
145	142 143 144	syl2anc	$⊢ (φ \land c \in A) \to G (F (c)) = \{⟨1, N⟩\}$
146	135	eleq2d	$⊢ φ \to (c \in A \leftrightarrow c \in \{\{⟨1, N⟩\}\})$
147	146	biimpd	$⊢ φ \to (c \in A \to c \in \{\{⟨1, N⟩\}\})$
148	147	imp	$⊢ (φ \land c \in A) \to c \in \{\{⟨1, N⟩\}\}$
149		vex	$⊢ c \in V$
150	149	elsn	$⊢ c \in \{\{⟨1, N⟩\}\} \leftrightarrow c = \{⟨1, N⟩\}$
151	148 150	sylib	$⊢ (φ \land c \in A) \to c = \{⟨1, N⟩\}$
152	151	eqcomd	$⊢ (φ \land c \in A) \to \{⟨1, N⟩\} = c$
153	145 152	eqtrd	$⊢ (φ \land c \in A) \to G (F (c)) = c$
154	153	ralrimiva	$⊢ φ \to \forall c \in A G (F (c)) = c$
155		simpr	$⊢ (φ \land d \in B) \to d \in B$
156		nfv	$⊢ Ⅎ d φ$
157		nfcv	$⊢ \underline{Ⅎ} d B$
158		nfcv	$⊢ \underline{Ⅎ} d \{\emptyset\}$
159	6	a1i	$⊢ (φ \land d \in B) \to B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
160	159	eleq2d	$⊢ (φ \land d \in B) \to (d \in B \leftrightarrow d \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\})$
161	160	biimpd	$⊢ (φ \land d \in B) \to (d \in B \to d \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\})$
162	161	syldbl2	$⊢ (φ \land d \in B) \to d \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
163		vex	$⊢ d \in V$
164		feq1	$⊢ f = d \to (f : (1 \dots K) ⟶ (1 \dots N + K) \leftrightarrow d : (1 \dots K) ⟶ (1 \dots N + K))$
165		fveq1	$⊢ f = d \to f (x) = d (x)$
166		fveq1	$⊢ f = d \to f (y) = d (y)$
167	165 166	breq12d	$⊢ f = d \to (f (x) < f (y) \leftrightarrow d (x) < d (y))$
168	167	imbi2d	$⊢ f = d \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to d (x) < d (y)))$
169	168	2ralbidv	$⊢ f = d \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)) \leftrightarrow \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to d (x) < d (y)))$
170	164 169	anbi12d	$⊢ f = d \to ((f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y))) \leftrightarrow (d : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to d (x) < d (y))))$
171	163 170	elab	$⊢ d \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \leftrightarrow (d : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to d (x) < d (y)))$
172	162 171	sylib	$⊢ (φ \land d \in B) \to (d : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to d (x) < d (y)))$
173	172	simpld	$⊢ (φ \land d \in B) \to d : (1 \dots K) ⟶ (1 \dots N + K)$
174		0lt1	$⊢ 0 < 1$
175	174	a1i	$⊢ φ \to 0 < 1$
176	2 175	eqbrtrd	$⊢ φ \to K < 1$
177	9	nn0zd	$⊢ φ \to K \in ℤ$
178		fzn	$⊢ (1 \in ℤ \land K \in ℤ) \to (K < 1 \leftrightarrow (1 \dots K) = \emptyset)$
179	67 177 178	syl2anc	$⊢ φ \to (K < 1 \leftrightarrow (1 \dots K) = \emptyset)$
180	176 179	mpbid	$⊢ φ \to (1 \dots K) = \emptyset$
181	180	feq2d	$⊢ φ \to (d : (1 \dots K) ⟶ (1 \dots N + K) \leftrightarrow d : \emptyset ⟶ (1 \dots N + K))$
182	181	adantr	$⊢ (φ \land d \in B) \to (d : (1 \dots K) ⟶ (1 \dots N + K) \leftrightarrow d : \emptyset ⟶ (1 \dots N + K))$
183	173 182	mpbid	$⊢ (φ \land d \in B) \to d : \emptyset ⟶ (1 \dots N + K)$
184		f0bi	$⊢ d : \emptyset ⟶ (1 \dots N + K) \leftrightarrow d = \emptyset$
185	183 184	sylib	$⊢ (φ \land d \in B) \to d = \emptyset$
186		velsn	$⊢ d \in \{\emptyset\} \leftrightarrow d = \emptyset$
187	185 186	sylibr	$⊢ (φ \land d \in B) \to d \in \{\emptyset\}$
188	187	ex	$⊢ φ \to (d \in B \to d \in \{\emptyset\})$
189		f0	$⊢ \emptyset : \emptyset ⟶ (1 \dots N + K)$
190	189	a1i	$⊢ φ \to \emptyset : \emptyset ⟶ (1 \dots N + K)$
191	180	feq2d	$⊢ φ \to (\emptyset : (1 \dots K) ⟶ (1 \dots N + K) \leftrightarrow \emptyset : \emptyset ⟶ (1 \dots N + K))$
192	190 191	mpbird	$⊢ φ \to \emptyset : (1 \dots K) ⟶ (1 \dots N + K)$
193		ral0	$⊢ \forall x \in \emptyset \forall y \in (1 \dots K) (x < y \to \emptyset (x) < \emptyset (y))$
194	193	a1i	$⊢ φ \to \forall x \in \emptyset \forall y \in (1 \dots K) (x < y \to \emptyset (x) < \emptyset (y))$
195	194 180	raleqtrrdv	$⊢ φ \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to \emptyset (x) < \emptyset (y))$
196	192 195	jca	$⊢ φ \to (\emptyset : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to \emptyset (x) < \emptyset (y)))$
197		0ex	$⊢ \emptyset \in V$
198		feq1	$⊢ f = \emptyset \to (f : (1 \dots K) ⟶ (1 \dots N + K) \leftrightarrow \emptyset : (1 \dots K) ⟶ (1 \dots N + K))$
199		fveq1	$⊢ f = \emptyset \to f (x) = \emptyset (x)$
200		fveq1	$⊢ f = \emptyset \to f (y) = \emptyset (y)$
201	199 200	breq12d	$⊢ f = \emptyset \to (f (x) < f (y) \leftrightarrow \emptyset (x) < \emptyset (y))$
202	201	imbi2d	$⊢ f = \emptyset \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to \emptyset (x) < \emptyset (y)))$
203	202	2ralbidv	$⊢ f = \emptyset \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)) \leftrightarrow \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to \emptyset (x) < \emptyset (y)))$
204	198 203	anbi12d	$⊢ f = \emptyset \to ((f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y))) \leftrightarrow (\emptyset : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to \emptyset (x) < \emptyset (y))))$
205	204	elabg	$⊢ \emptyset \in V \to (\emptyset \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \leftrightarrow (\emptyset : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to \emptyset (x) < \emptyset (y))))$
206	197 205	ax-mp	$⊢ \emptyset \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \leftrightarrow (\emptyset : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to \emptyset (x) < \emptyset (y)))$
207	196 206	sylibr	$⊢ φ \to \emptyset \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
208	6	a1i	$⊢ φ \to B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
209	207 208	eleqtrrd	$⊢ φ \to \emptyset \in B$
210	209	adantr	$⊢ (φ \land d \in \{\emptyset\}) \to \emptyset \in B$
211		elsni	$⊢ d \in \{\emptyset\} \to d = \emptyset$
212	211	adantl	$⊢ (φ \land d \in \{\emptyset\}) \to d = \emptyset$
213	212	eleq1d	$⊢ (φ \land d \in \{\emptyset\}) \to (d \in B \leftrightarrow \emptyset \in B)$
214	210 213	mpbird	$⊢ (φ \land d \in \{\emptyset\}) \to d \in B$
215	214	ex	$⊢ φ \to (d \in \{\emptyset\} \to d \in B)$
216	188 215	impbid	$⊢ φ \to (d \in B \leftrightarrow d \in \{\emptyset\})$
217	156 157 158 216	eqrd	$⊢ φ \to B = \{\emptyset\}$
218	217	adantr	$⊢ (φ \land d \in B) \to B = \{\emptyset\}$
219	155 218	eleqtrd	$⊢ (φ \land d \in B) \to d \in \{\emptyset\}$
220	163	elsn	$⊢ d \in \{\emptyset\} \leftrightarrow d = \emptyset$
221	219 220	sylib	$⊢ (φ \land d \in B) \to d = \emptyset$
222	221	fveq2d	$⊢ (φ \land d \in B) \to G (d) = G (\emptyset)$
223	222	fveq2d	$⊢ (φ \land d \in B) \to F (G (d)) = F (G (\emptyset))$
224	180	adantr	$⊢ (φ \land a \in A) \to (1 \dots K) = \emptyset$
225	224	mpteq1d	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) = (j \in \emptyset ⟼ j + \sum_{l = 1}^{j} a (l))$
226		mpt0	$⊢ (j \in \emptyset ⟼ j + \sum_{l = 1}^{j} a (l)) = \emptyset$
227	226	a1i	$⊢ (φ \land a \in A) \to (j \in \emptyset ⟼ j + \sum_{l = 1}^{j} a (l)) = \emptyset$
228	225 227	eqtrd	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) = \emptyset$
229		fzfid	$⊢ φ \to (1 \dots K) \in Fin$
230	229	mptexd	$⊢ φ \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in V$
231		elsng	$⊢ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in V \to ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in \{\emptyset\} \leftrightarrow (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) = \emptyset)$
232	230 231	syl	$⊢ φ \to ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in \{\emptyset\} \leftrightarrow (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) = \emptyset)$
233	232	adantr	$⊢ (φ \land a \in A) \to ((j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in \{\emptyset\} \leftrightarrow (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) = \emptyset)$
234	228 233	mpbird	$⊢ (φ \land a \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) \in \{\emptyset\}$
235	234 3	fmptd	$⊢ φ \to F : A ⟶ \{\emptyset\}$
236	235	adantr	$⊢ (φ \land d \in B) \to F : A ⟶ \{\emptyset\}$
237		ffvelcdm	$⊢ (G : B ⟶ A \land \emptyset \in B) \to G (\emptyset) \in A$
238	11 209 237	syl2anc	$⊢ φ \to G (\emptyset) \in A$
239	238	adantr	$⊢ (φ \land d \in B) \to G (\emptyset) \in A$
240		fvconst	$⊢ (F : A ⟶ \{\emptyset\} \land G (\emptyset) \in A) \to F (G (\emptyset)) = \emptyset$
241	236 239 240	syl2anc	$⊢ (φ \land d \in B) \to F (G (\emptyset)) = \emptyset$
242	223 241	eqtrd	$⊢ (φ \land d \in B) \to F (G (d)) = \emptyset$
243	221	eqcomd	$⊢ (φ \land d \in B) \to \emptyset = d$
244	242 243	eqtrd	$⊢ (φ \land d \in B) \to F (G (d)) = d$
245	244	ralrimiva	$⊢ φ \to \forall d \in B F (G (d)) = d$
246	10 11 154 245	2fvidf1od	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem sticksstones11

Proof