dvnprodlem1

	Ref	Expression
Hypotheses	dvnprodlem1.c	$⊢ C = (s \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\}))$
	dvnprodlem1.j	$⊢ φ \to J \in ℕ_{0}$
	dvnprodlem1.d	$⊢ D = (c \in C (R \cup \{Z\}) (J) ⟼ ⟨J - c (Z), {c ↾}_{R}⟩)$
	dvnprodlem1.t	$⊢ φ \to T \in Fin$
	dvnprodlem1.z	$⊢ φ \to Z \in T$
	dvnprodlem1.zr	$⊢ φ \to \neg Z \in R$
	dvnprodlem1.rzt	$⊢ φ \to R \cup \{Z\} \subseteq T$
Assertion	dvnprodlem1	$⊢ φ \to D : C (R \cup \{Z\}) (J) \underset{1-1 onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$

Proof

Step	Hyp	Ref	Expression
1		dvnprodlem1.c	$⊢ C = (s \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\}))$
2		dvnprodlem1.j	$⊢ φ \to J \in ℕ_{0}$
3		dvnprodlem1.d	$⊢ D = (c \in C (R \cup \{Z\}) (J) ⟼ ⟨J - c (Z), {c ↾}_{R}⟩)$
4		dvnprodlem1.t	$⊢ φ \to T \in Fin$
5		dvnprodlem1.z	$⊢ φ \to Z \in T$
6		dvnprodlem1.zr	$⊢ φ \to \neg Z \in R$
7		dvnprodlem1.rzt	$⊢ φ \to R \cup \{Z\} \subseteq T$
8		eqidd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ⟨J - c (Z), {c ↾}_{R}⟩ = ⟨J - c (Z), {c ↾}_{R}⟩$
9		0zd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to 0 \in ℤ$
10	2	nn0zd	$⊢ φ \to J \in ℤ$
11	10	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J \in ℤ$
12		oveq2	$⊢ s = R \cup \{Z\} \to {(0 \dots n)}^{s} = {(0 \dots n)}^{(R \cup \{Z\})}$
13		rabeq	$⊢ {(0 \dots n)}^{s} = {(0 \dots n)}^{(R \cup \{Z\})} \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in s} c (t) = n\}$
14	12 13	syl	$⊢ s = R \cup \{Z\} \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in s} c (t) = n\}$
15		sumeq1	$⊢ s = R \cup \{Z\} \to \sum_{t \in s} c (t) = \sum_{t \in R \cup \{Z\}} c (t)$
16	15	eqeq1d	$⊢ s = R \cup \{Z\} \to (\sum_{t \in s} c (t) = n \leftrightarrow \sum_{t \in R \cup \{Z\}} c (t) = n)$
17	16	rabbidv	$⊢ s = R \cup \{Z\} \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}$
18	14 17	eqtrd	$⊢ s = R \cup \{Z\} \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}$
19	18	mpteq2dv	$⊢ s = R \cup \{Z\} \to (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\}) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\})$
20		ssexg	$⊢ (R \cup \{Z\} \subseteq T \land T \in Fin) \to R \cup \{Z\} \in V$
21	7 4 20	syl2anc	$⊢ φ \to R \cup \{Z\} \in V$
22		elpwg	$⊢ R \cup \{Z\} \in V \to (R \cup \{Z\} \in 𝒫 T \leftrightarrow R \cup \{Z\} \subseteq T)$
23	21 22	syl	$⊢ φ \to (R \cup \{Z\} \in 𝒫 T \leftrightarrow R \cup \{Z\} \subseteq T)$
24	7 23	mpbird	$⊢ φ \to R \cup \{Z\} \in 𝒫 T$
25		nn0ex	$⊢ ℕ_{0} \in V$
26	25	mptex	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}) \in V$
27	26	a1i	$⊢ φ \to (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}) \in V$
28	1 19 24 27	fvmptd3	$⊢ φ \to C (R \cup \{Z\}) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\})$
29		oveq2	$⊢ n = J \to (0 \dots n) = (0 \dots J)$
30	29	oveq1d	$⊢ n = J \to {(0 \dots n)}^{(R \cup \{Z\})} = {(0 \dots J)}^{(R \cup \{Z\})}$
31		rabeq	$⊢ {(0 \dots n)}^{(R \cup \{Z\})} = {(0 \dots J)}^{(R \cup \{Z\})} \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}$
32	30 31	syl	$⊢ n = J \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\}$
33		eqeq2	$⊢ n = J \to (\sum_{t \in R \cup \{Z\}} c (t) = n \leftrightarrow \sum_{t \in R \cup \{Z\}} c (t) = J)$
34	33	rabbidv	$⊢ n = J \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
35	32 34	eqtrd	$⊢ n = J \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
36	35	adantl	$⊢ (φ \land n = J) \to \{c \in ({(0 \dots n)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = n\} = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
37		ovex	$⊢ {(0 \dots J)}^{(R \cup \{Z\})} \in V$
38	37	rabex	$⊢ \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in V$
39	38	a1i	$⊢ φ \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \in V$
40	28 36 2 39	fvmptd	$⊢ φ \to C (R \cup \{Z\}) (J) = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
41		ssrab2	$⊢ \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \subseteq {(0 \dots J)}^{(R \cup \{Z\})}$
42	41	a1i	$⊢ φ \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \subseteq {(0 \dots J)}^{(R \cup \{Z\})}$
43	40 42	eqsstrd	$⊢ φ \to C (R \cup \{Z\}) (J) \subseteq {(0 \dots J)}^{(R \cup \{Z\})}$
44	43	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to C (R \cup \{Z\}) (J) \subseteq {(0 \dots J)}^{(R \cup \{Z\})}$
45		simpr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in C (R \cup \{Z\}) (J)$
46	44 45	sseldd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in ({(0 \dots J)}^{(R \cup \{Z\})})$
47		elmapi	$⊢ c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
48	46 47	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
49		snidg	$⊢ Z \in T \to Z \in \{Z\}$
50	5 49	syl	$⊢ φ \to Z \in \{Z\}$
51		elun2	$⊢ Z \in \{Z\} \to Z \in (R \cup \{Z\})$
52	50 51	syl	$⊢ φ \to Z \in (R \cup \{Z\})$
53	52	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to Z \in (R \cup \{Z\})$
54	48 53	ffvelcdmd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in (0 \dots J)$
55	54	elfzelzd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℤ$
56	11 55	zsubcld	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in ℤ$
57		elfzle2	$⊢ c (Z) \in (0 \dots J) \to c (Z) \leq J$
58	54 57	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \leq J$
59	11	zred	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J \in ℝ$
60	55	zred	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℝ$
61	59 60	subge0d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \leq J - c (Z) \leftrightarrow c (Z) \leq J)$
62	58 61	mpbird	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to 0 \leq J - c (Z)$
63		elfzle1	$⊢ c (Z) \in (0 \dots J) \to 0 \leq c (Z)$
64	54 63	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to 0 \leq c (Z)$
65	59 60	subge02d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \leq c (Z) \leftrightarrow J - c (Z) \leq J)$
66	64 65	mpbid	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \leq J$
67	9 11 56 62 66	elfzd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in (0 \dots J)$
68		elmapfn	$⊢ c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \to c Fn (R \cup \{Z\})$
69	46 68	syl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c Fn (R \cup \{Z\})$
70		ssun1	$⊢ R \subseteq R \cup \{Z\}$
71	70	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \subseteq R \cup \{Z\}$
72		fnssres	$⊢ (c Fn (R \cup \{Z\}) \land R \subseteq R \cup \{Z\}) \to ({c ↾}_{R}) Fn R$
73	69 71 72	syl2anc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ({c ↾}_{R}) Fn R$
74		nfv	$⊢ Ⅎ t φ$
75		nfcv	$⊢ \underline{Ⅎ} t c$
76		nfcv	$⊢ \underline{Ⅎ} t 𝒫 T$
77		nfcv	$⊢ \underline{Ⅎ} t ℕ_{0}$
78		nfcv	$⊢ \underline{Ⅎ} t s$
79	78	nfsum1	$⊢ \underline{Ⅎ} t \sum_{t \in s} c (t)$
80		nfcv	$⊢ \underline{Ⅎ} t n$
81	79 80	nfeq	$⊢ Ⅎ t \sum_{t \in s} c (t) = n$
82		nfcv	$⊢ \underline{Ⅎ} t ({(0 \dots n)}^{s})$
83	81 82	nfrabw	$⊢ \underline{Ⅎ} t \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\}$
84	77 83	nfmpt	$⊢ \underline{Ⅎ} t (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\})$
85	76 84	nfmpt	$⊢ \underline{Ⅎ} t (s \in 𝒫 T ⟼ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\}))$
86	1 85	nfcxfr	$⊢ \underline{Ⅎ} t C$
87		nfcv	$⊢ \underline{Ⅎ} t (R \cup \{Z\})$
88	86 87	nffv	$⊢ \underline{Ⅎ} t C (R \cup \{Z\})$
89		nfcv	$⊢ \underline{Ⅎ} t J$
90	88 89	nffv	$⊢ \underline{Ⅎ} t C (R \cup \{Z\}) (J)$
91	75 90	nfel	$⊢ Ⅎ t c \in C (R \cup \{Z\}) (J)$
92	74 91	nfan	$⊢ Ⅎ t (φ \land c \in C (R \cup \{Z\}) (J))$
93		fvres	$⊢ t \in R \to ({c ↾}_{R}) (t) = c (t)$
94	93	adantl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to ({c ↾}_{R}) (t) = c (t)$
95	9	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to 0 \in ℤ$
96	56	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to J - c (Z) \in ℤ$
97	48	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
98	71	sselda	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to t \in (R \cup \{Z\})$
99	97 98	ffvelcdmd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in (0 \dots J)$
100	99	elfzelzd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in ℤ$
101		elfzle1	$⊢ c (t) \in (0 \dots J) \to 0 \leq c (t)$
102	99 101	syl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to 0 \leq c (t)$
103	7	unssad	$⊢ φ \to R \subseteq T$
104		ssfi	$⊢ (T \in Fin \land R \subseteq T) \to R \in Fin$
105	4 103 104	syl2anc	$⊢ φ \to R \in Fin$
106	105	ad2antrr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to R \in Fin$
107		fzssz	$⊢ (0 \dots J) \subseteq ℤ$
108		zssre	$⊢ ℤ \subseteq ℝ$
109	107 108	sstri	$⊢ (0 \dots J) \subseteq ℝ$
110	109	a1i	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land r \in R) \to (0 \dots J) \subseteq ℝ$
111	48	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land r \in R) \to c : R \cup \{Z\} ⟶ (0 \dots J)$
112	71	sselda	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land r \in R) \to r \in (R \cup \{Z\})$
113	111 112	ffvelcdmd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land r \in R) \to c (r) \in (0 \dots J)$
114	110 113	sseldd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land r \in R) \to c (r) \in ℝ$
115	114	adantlr	$⊢ (((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \land r \in R) \to c (r) \in ℝ$
116		elfzle1	$⊢ c (r) \in (0 \dots J) \to 0 \leq c (r)$
117	113 116	syl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land r \in R) \to 0 \leq c (r)$
118	117	adantlr	$⊢ (((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \land r \in R) \to 0 \leq c (r)$
119		fveq2	$⊢ r = t \to c (r) = c (t)$
120		simpr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to t \in R$
121	106 115 118 119 120	fsumge1	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \leq \sum_{r \in R} c (r)$
122	105	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \in Fin$
123	114	recnd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land r \in R) \to c (r) \in ℂ$
124	122 123	fsumcl	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R} c (r) \in ℂ$
125	60	recnd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) \in ℂ$
126	124 125	pncand	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R} c (r) + c (Z) - c (Z) = \sum_{r \in R} c (r)$
127		nfv	$⊢ Ⅎ r (φ \land c \in C (R \cup \{Z\}) (J))$
128		nfcv	$⊢ \underline{Ⅎ} r c (Z)$
129	5	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to Z \in T$
130	6	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \neg Z \in R$
131		fveq2	$⊢ r = Z \to c (r) = c (Z)$
132	127 128 122 129 130 123 131 125	fsumsplitsn	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R \cup \{Z\}} c (r) = \sum_{r \in R} c (r) + c (Z)$
133	132	eqcomd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R} c (r) + c (Z) = \sum_{r \in R \cup \{Z\}} c (r)$
134	119	cbvsumv	$⊢ \sum_{r \in R \cup \{Z\}} c (r) = \sum_{t \in R \cup \{Z\}} c (t)$
135	134	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R \cup \{Z\}} c (r) = \sum_{t \in R \cup \{Z\}} c (t)$
136	40	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to C (R \cup \{Z\}) (J) = \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
137	45 136	eleqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
138		rabid	$⊢ c \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \leftrightarrow (c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \land \sum_{t \in R \cup \{Z\}} c (t) = J)$
139	137 138	sylib	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \land \sum_{t \in R \cup \{Z\}} c (t) = J)$
140	139	simprd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{t \in R \cup \{Z\}} c (t) = J$
141	135 140	eqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R \cup \{Z\}} c (r) = J$
142	133 141	eqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R} c (r) + c (Z) = J$
143	142	oveq1d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R} c (r) + c (Z) - c (Z) = J - c (Z)$
144	126 143	eqtr3d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R} c (r) = J - c (Z)$
145	144	adantr	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to \sum_{r \in R} c (r) = J - c (Z)$
146	121 145	breqtrd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \leq J - c (Z)$
147	95 96 100 102 146	elfzd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) \in (0 \dots J - c (Z))$
148	94 147	eqeltrd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to ({c ↾}_{R}) (t) \in (0 \dots J - c (Z))$
149	148	ex	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (t \in R \to ({c ↾}_{R}) (t) \in (0 \dots J - c (Z)))$
150	92 149	ralrimi	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \forall t \in R ({c ↾}_{R}) (t) \in (0 \dots J - c (Z))$
151	73 150	jca	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (({c ↾}_{R}) Fn R \land \forall t \in R ({c ↾}_{R}) (t) \in (0 \dots J - c (Z)))$
152		ffnfv	$⊢ ({c ↾}_{R}) : R ⟶ (0 \dots J - c (Z)) \leftrightarrow (({c ↾}_{R}) Fn R \land \forall t \in R ({c ↾}_{R}) (t) \in (0 \dots J - c (Z)))$
153	151 152	sylibr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ({c ↾}_{R}) : R ⟶ (0 \dots J - c (Z))$
154		ovexd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (0 \dots J - c (Z)) \in V$
155	4 103	ssexd	$⊢ φ \to R \in V$
156	155	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to R \in V$
157	154 156	elmapd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ({c ↾}_{R} \in ({(0 \dots J - c (Z))}^{R}) \leftrightarrow ({c ↾}_{R}) : R ⟶ (0 \dots J - c (Z)))$
158	153 157	mpbird	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to {c ↾}_{R} \in ({(0 \dots J - c (Z))}^{R})$
159	93	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (t \in R \to ({c ↾}_{R}) (t) = c (t))$
160	92 159	ralrimi	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \forall t \in R ({c ↾}_{R}) (t) = c (t)$
161	160	sumeq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{t \in R} ({c ↾}_{R}) (t) = \sum_{t \in R} c (t)$
162	119	cbvsumv	$⊢ \sum_{r \in R} c (r) = \sum_{t \in R} c (t)$
163	162	eqcomi	$⊢ \sum_{t \in R} c (t) = \sum_{r \in R} c (r)$
164	163	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{t \in R} c (t) = \sum_{r \in R} c (r)$
165	144	idi	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{r \in R} c (r) = J - c (Z)$
166	161 164 165	3eqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \sum_{t \in R} ({c ↾}_{R}) (t) = J - c (Z)$
167	158 166	jca	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ({c ↾}_{R} \in ({(0 \dots J - c (Z))}^{R}) \land \sum_{t \in R} ({c ↾}_{R}) (t) = J - c (Z))$
168		eqidd	$⊢ e = {c ↾}_{R} \to R = R$
169		simpl	$⊢ (e = {c ↾}_{R} \land t \in R) \to e = {c ↾}_{R}$
170	169	fveq1d	$⊢ (e = {c ↾}_{R} \land t \in R) \to e (t) = ({c ↾}_{R}) (t)$
171	168 170	sumeq12rdv	$⊢ e = {c ↾}_{R} \to \sum_{t \in R} e (t) = \sum_{t \in R} ({c ↾}_{R}) (t)$
172	171	eqeq1d	$⊢ e = {c ↾}_{R} \to (\sum_{t \in R} e (t) = J - c (Z) \leftrightarrow \sum_{t \in R} ({c ↾}_{R}) (t) = J - c (Z))$
173	172	elrab	$⊢ {c ↾}_{R} \in \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\} \leftrightarrow ({c ↾}_{R} \in ({(0 \dots J - c (Z))}^{R}) \land \sum_{t \in R} ({c ↾}_{R}) (t) = J - c (Z))$
174	167 173	sylibr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to {c ↾}_{R} \in \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\}$
175		oveq2	$⊢ s = R \to {(0 \dots n)}^{s} = {(0 \dots n)}^{R}$
176		rabeq	$⊢ {(0 \dots n)}^{s} = {(0 \dots n)}^{R} \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in s} c (t) = n\}$
177	175 176	syl	$⊢ s = R \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in s} c (t) = n\}$
178		sumeq1	$⊢ s = R \to \sum_{t \in s} c (t) = \sum_{t \in R} c (t)$
179	178	eqeq1d	$⊢ s = R \to (\sum_{t \in s} c (t) = n \leftrightarrow \sum_{t \in R} c (t) = n)$
180	179	rabbidv	$⊢ s = R \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}$
181	177 180	eqtrd	$⊢ s = R \to \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\} = \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}$
182	181	mpteq2dv	$⊢ s = R \to (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{s}) \| \sum_{t \in s} c (t) = n\}) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\})$
183		elpwg	$⊢ R \in V \to (R \in 𝒫 T \leftrightarrow R \subseteq T)$
184	155 183	syl	$⊢ φ \to (R \in 𝒫 T \leftrightarrow R \subseteq T)$
185	103 184	mpbird	$⊢ φ \to R \in 𝒫 T$
186	25	mptex	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}) \in V$
187	186	a1i	$⊢ φ \to (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}) \in V$
188	1 182 185 187	fvmptd3	$⊢ φ \to C (R) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\})$
189	188	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to C (R) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\})$
190		oveq2	$⊢ n = m \to (0 \dots n) = (0 \dots m)$
191	190	oveq1d	$⊢ n = m \to {(0 \dots n)}^{R} = {(0 \dots m)}^{R}$
192		rabeq	$⊢ {(0 \dots n)}^{R} = {(0 \dots m)}^{R} \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = n\}$
193	191 192	syl	$⊢ n = m \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = n\}$
194		eqeq2	$⊢ n = m \to (\sum_{t \in R} c (t) = n \leftrightarrow \sum_{t \in R} c (t) = m)$
195	194	rabbidv	$⊢ n = m \to \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\}$
196	193 195	eqtrd	$⊢ n = m \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\}$
197	196	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}) = (m \in ℕ_{0} ⟼ \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\})$
198	197	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\}) = (m \in ℕ_{0} ⟼ \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\})$
199	189 198	eqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to C (R) = (m \in ℕ_{0} ⟼ \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\})$
200		fveq1	$⊢ c = e \to c (t) = e (t)$
201	200	sumeq2sdv	$⊢ c = e \to \sum_{t \in R} c (t) = \sum_{t \in R} e (t)$
202	201	eqeq1d	$⊢ c = e \to (\sum_{t \in R} c (t) = m \leftrightarrow \sum_{t \in R} e (t) = m)$
203	202	cbvrabv	$⊢ \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\} = \{e \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} e (t) = m\}$
204	203	a1i	$⊢ m = J - c (Z) \to \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\} = \{e \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} e (t) = m\}$
205		oveq2	$⊢ m = J - c (Z) \to (0 \dots m) = (0 \dots J - c (Z))$
206	205	oveq1d	$⊢ m = J - c (Z) \to {(0 \dots m)}^{R} = {(0 \dots J - c (Z))}^{R}$
207		rabeq	$⊢ {(0 \dots m)}^{R} = {(0 \dots J - c (Z))}^{R} \to \{e \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} e (t) = m\} = \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = m\}$
208	206 207	syl	$⊢ m = J - c (Z) \to \{e \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} e (t) = m\} = \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = m\}$
209		eqeq2	$⊢ m = J - c (Z) \to (\sum_{t \in R} e (t) = m \leftrightarrow \sum_{t \in R} e (t) = J - c (Z))$
210	209	rabbidv	$⊢ m = J - c (Z) \to \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = m\} = \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\}$
211	204 208 210	3eqtrd	$⊢ m = J - c (Z) \to \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\} = \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\}$
212	211	adantl	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land m = J - c (Z)) \to \{c \in ({(0 \dots m)}^{R}) \| \sum_{t \in R} c (t) = m\} = \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\}$
213	56 62	jca	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z) \in ℤ \land 0 \leq J - c (Z))$
214		elnn0z	$⊢ J - c (Z) \in ℕ_{0} \leftrightarrow (J - c (Z) \in ℤ \land 0 \leq J - c (Z))$
215	213 214	sylibr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in ℕ_{0}$
216		ovex	$⊢ {(0 \dots J - c (Z))}^{R} \in V$
217	216	rabex	$⊢ \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\} \in V$
218	217	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\} \in V$
219	199 212 215 218	fvmptd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to C (R) (J - c (Z)) = \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\}$
220	219	eqcomd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \{e \in ({(0 \dots J - c (Z))}^{R}) \| \sum_{t \in R} e (t) = J - c (Z)\} = C (R) (J - c (Z))$
221	174 220	eleqtrd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to {c ↾}_{R} \in C (R) (J - c (Z))$
222	67 221	jca	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (J - c (Z) \in (0 \dots J) \land {c ↾}_{R} \in C (R) (J - c (Z)))$
223	8 222	jca	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to (⟨J - c (Z), {c ↾}_{R}⟩ = ⟨J - c (Z), {c ↾}_{R}⟩ \land (J - c (Z) \in (0 \dots J) \land {c ↾}_{R} \in C (R) (J - c (Z))))$
224		ovexd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) \in V$
225		vex	$⊢ c \in V$
226	225	resex	$⊢ {c ↾}_{R} \in V$
227	226	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to {c ↾}_{R} \in V$
228		opeq12	$⊢ (k = J - c (Z) \land d = {c ↾}_{R}) \to ⟨k, d⟩ = ⟨J - c (Z), {c ↾}_{R}⟩$
229	228	eqeq2d	$⊢ (k = J - c (Z) \land d = {c ↾}_{R}) \to (⟨J - c (Z), {c ↾}_{R}⟩ = ⟨k, d⟩ \leftrightarrow ⟨J - c (Z), {c ↾}_{R}⟩ = ⟨J - c (Z), {c ↾}_{R}⟩)$
230		eleq1	$⊢ k = J - c (Z) \to (k \in (0 \dots J) \leftrightarrow J - c (Z) \in (0 \dots J))$
231	230	adantr	$⊢ (k = J - c (Z) \land d = {c ↾}_{R}) \to (k \in (0 \dots J) \leftrightarrow J - c (Z) \in (0 \dots J))$
232		simpr	$⊢ (k = J - c (Z) \land d = {c ↾}_{R}) \to d = {c ↾}_{R}$
233		fveq2	$⊢ k = J - c (Z) \to C (R) (k) = C (R) (J - c (Z))$
234	233	adantr	$⊢ (k = J - c (Z) \land d = {c ↾}_{R}) \to C (R) (k) = C (R) (J - c (Z))$
235	232 234	eleq12d	$⊢ (k = J - c (Z) \land d = {c ↾}_{R}) \to (d \in C (R) (k) \leftrightarrow {c ↾}_{R} \in C (R) (J - c (Z)))$
236	231 235	anbi12d	$⊢ (k = J - c (Z) \land d = {c ↾}_{R}) \to ((k \in (0 \dots J) \land d \in C (R) (k)) \leftrightarrow (J - c (Z) \in (0 \dots J) \land {c ↾}_{R} \in C (R) (J - c (Z))))$
237	229 236	anbi12d	$⊢ (k = J - c (Z) \land d = {c ↾}_{R}) \to ((⟨J - c (Z), {c ↾}_{R}⟩ = ⟨k, d⟩ \land (k \in (0 \dots J) \land d \in C (R) (k))) \leftrightarrow (⟨J - c (Z), {c ↾}_{R}⟩ = ⟨J - c (Z), {c ↾}_{R}⟩ \land (J - c (Z) \in (0 \dots J) \land {c ↾}_{R} \in C (R) (J - c (Z)))))$
238	237	spc2egv	$⊢ (J - c (Z) \in V \land {c ↾}_{R} \in V) \to ((⟨J - c (Z), {c ↾}_{R}⟩ = ⟨J - c (Z), {c ↾}_{R}⟩ \land (J - c (Z) \in (0 \dots J) \land {c ↾}_{R} \in C (R) (J - c (Z)))) \to \exists k \exists d (⟨J - c (Z), {c ↾}_{R}⟩ = ⟨k, d⟩ \land (k \in (0 \dots J) \land d \in C (R) (k))))$
239	224 227 238	syl2anc	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ((⟨J - c (Z), {c ↾}_{R}⟩ = ⟨J - c (Z), {c ↾}_{R}⟩ \land (J - c (Z) \in (0 \dots J) \land {c ↾}_{R} \in C (R) (J - c (Z)))) \to \exists k \exists d (⟨J - c (Z), {c ↾}_{R}⟩ = ⟨k, d⟩ \land (k \in (0 \dots J) \land d \in C (R) (k))))$
240	223 239	mpd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to \exists k \exists d (⟨J - c (Z), {c ↾}_{R}⟩ = ⟨k, d⟩ \land (k \in (0 \dots J) \land d \in C (R) (k)))$
241		eliunxp	$⊢ ⟨J - c (Z), {c ↾}_{R}⟩ \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \leftrightarrow \exists k \exists d (⟨J - c (Z), {c ↾}_{R}⟩ = ⟨k, d⟩ \land (k \in (0 \dots J) \land d \in C (R) (k)))$
242	240 241	sylibr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ⟨J - c (Z), {c ↾}_{R}⟩ \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
243	242 3	fmptd	$⊢ φ \to D : C (R \cup \{Z\}) (J) ⟶ ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
244	90	nfcri	$⊢ Ⅎ t e \in C (R \cup \{Z\}) (J)$
245	91 244	nfan	$⊢ Ⅎ t (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))$
246	74 245	nfan	$⊢ Ⅎ t (φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J)))$
247		nfv	$⊢ Ⅎ t D (c) = D (e)$
248	246 247	nfan	$⊢ Ⅎ t ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e))$
249	94	eqcomd	$⊢ ((φ \land c \in C (R \cup \{Z\}) (J)) \land t \in R) \to c (t) = ({c ↾}_{R}) (t)$
250	249	adantlrr	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land t \in R) \to c (t) = ({c ↾}_{R}) (t)$
251	250	adantlr	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to c (t) = ({c ↾}_{R}) (t)$
252	3	a1i	$⊢ φ \to D = (c \in C (R \cup \{Z\}) (J) ⟼ ⟨J - c (Z), {c ↾}_{R}⟩)$
253		opex	$⊢ ⟨J - c (Z), {c ↾}_{R}⟩ \in V$
254	253	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ⟨J - c (Z), {c ↾}_{R}⟩ \in V$
255	252 254	fvmpt2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to D (c) = ⟨J - c (Z), {c ↾}_{R}⟩$
256	255	fveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to 2^{nd} (D (c)) = 2^{nd} (⟨J - c (Z), {c ↾}_{R}⟩)$
257	256	fveq1d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to 2^{nd} (D (c)) (t) = 2^{nd} (⟨J - c (Z), {c ↾}_{R}⟩) (t)$
258		ovex	$⊢ J - c (Z) \in V$
259	258 226	op2nd	$⊢ 2^{nd} (⟨J - c (Z), {c ↾}_{R}⟩) = {c ↾}_{R}$
260	259	fveq1i	$⊢ 2^{nd} (⟨J - c (Z), {c ↾}_{R}⟩) (t) = ({c ↾}_{R}) (t)$
261	260	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to 2^{nd} (⟨J - c (Z), {c ↾}_{R}⟩) (t) = ({c ↾}_{R}) (t)$
262	257 261	eqtr2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to ({c ↾}_{R}) (t) = 2^{nd} (D (c)) (t)$
263	262	adantrr	$⊢ (φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \to ({c ↾}_{R}) (t) = 2^{nd} (D (c)) (t)$
264	263	ad2antrr	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to ({c ↾}_{R}) (t) = 2^{nd} (D (c)) (t)$
265		simpr	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to D (c) = D (e)$
266		fveq1	$⊢ c = e \to c (Z) = e (Z)$
267	266	oveq2d	$⊢ c = e \to J - c (Z) = J - e (Z)$
268		reseq1	$⊢ c = e \to {c ↾}_{R} = {e ↾}_{R}$
269	267 268	opeq12d	$⊢ c = e \to ⟨J - c (Z), {c ↾}_{R}⟩ = ⟨J - e (Z), {e ↾}_{R}⟩$
270		simpr	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to e \in C (R \cup \{Z\}) (J)$
271		opex	$⊢ ⟨J - e (Z), {e ↾}_{R}⟩ \in V$
272	271	a1i	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to ⟨J - e (Z), {e ↾}_{R}⟩ \in V$
273	3 269 270 272	fvmptd3	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to D (e) = ⟨J - e (Z), {e ↾}_{R}⟩$
274	273	adantr	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to D (e) = ⟨J - e (Z), {e ↾}_{R}⟩$
275	265 274	eqtrd	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to D (c) = ⟨J - e (Z), {e ↾}_{R}⟩$
276	275	fveq2d	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to 2^{nd} (D (c)) = 2^{nd} (⟨J - e (Z), {e ↾}_{R}⟩)$
277	276	adantlrl	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to 2^{nd} (D (c)) = 2^{nd} (⟨J - e (Z), {e ↾}_{R}⟩)$
278	277	adantr	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to 2^{nd} (D (c)) = 2^{nd} (⟨J - e (Z), {e ↾}_{R}⟩)$
279		ovex	$⊢ J - e (Z) \in V$
280		vex	$⊢ e \in V$
281	280	resex	$⊢ {e ↾}_{R} \in V$
282	279 281	op2nd	$⊢ 2^{nd} (⟨J - e (Z), {e ↾}_{R}⟩) = {e ↾}_{R}$
283	282	a1i	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to 2^{nd} (⟨J - e (Z), {e ↾}_{R}⟩) = {e ↾}_{R}$
284	278 283	eqtrd	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to 2^{nd} (D (c)) = {e ↾}_{R}$
285	284	fveq1d	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to 2^{nd} (D (c)) (t) = ({e ↾}_{R}) (t)$
286		fvres	$⊢ t \in R \to ({e ↾}_{R}) (t) = e (t)$
287	286	adantl	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to ({e ↾}_{R}) (t) = e (t)$
288	285 287	eqtrd	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to 2^{nd} (D (c)) (t) = e (t)$
289	251 264 288	3eqtrd	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in R) \to c (t) = e (t)$
290	289	adantlr	$⊢ ((((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in (R \cup \{Z\})) \land t \in R) \to c (t) = e (t)$
291		simpl	$⊢ ((((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in (R \cup \{Z\}))$
292		elunnel1	$⊢ (t \in (R \cup \{Z\}) \land \neg t \in R) \to t \in \{Z\}$
293		elsni	$⊢ t \in \{Z\} \to t = Z$
294	292 293	syl	$⊢ (t \in (R \cup \{Z\}) \land \neg t \in R) \to t = Z$
295	294	adantll	$⊢ ((((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to t = Z$
296		simpr	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t = Z) \to t = Z$
297	296	fveq2d	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t = Z) \to c (t) = c (Z)$
298	2	nn0cnd	$⊢ φ \to J \in ℂ$
299	298	adantr	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J \in ℂ$
300	299 125	nncand	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - (J - c (Z)) = c (Z)$
301	300	eqcomd	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to c (Z) = J - (J - c (Z))$
302	301	adantrr	$⊢ (φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \to c (Z) = J - (J - c (Z))$
303	302	adantr	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to c (Z) = J - (J - c (Z))$
304	255	fveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to 1^{st} (D (c)) = 1^{st} (⟨J - c (Z), {c ↾}_{R}⟩)$
305	258 226	op1st	$⊢ 1^{st} (⟨J - c (Z), {c ↾}_{R}⟩) = J - c (Z)$
306	305	a1i	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to 1^{st} (⟨J - c (Z), {c ↾}_{R}⟩) = J - c (Z)$
307	304 306	eqtr2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - c (Z) = 1^{st} (D (c))$
308	307	oveq2d	$⊢ (φ \land c \in C (R \cup \{Z\}) (J)) \to J - (J - c (Z)) = J - 1^{st} (D (c))$
309	308	adantrr	$⊢ (φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \to J - (J - c (Z)) = J - 1^{st} (D (c))$
310	309	adantr	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to J - (J - c (Z)) = J - 1^{st} (D (c))$
311		fveq2	$⊢ D (c) = D (e) \to 1^{st} (D (c)) = 1^{st} (D (e))$
312	311	adantl	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to 1^{st} (D (c)) = 1^{st} (D (e))$
313	273	fveq2d	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to 1^{st} (D (e)) = 1^{st} (⟨J - e (Z), {e ↾}_{R}⟩)$
314	313	adantr	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to 1^{st} (D (e)) = 1^{st} (⟨J - e (Z), {e ↾}_{R}⟩)$
315	279 281	op1st	$⊢ 1^{st} (⟨J - e (Z), {e ↾}_{R}⟩) = J - e (Z)$
316	315	a1i	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to 1^{st} (⟨J - e (Z), {e ↾}_{R}⟩) = J - e (Z)$
317	312 314 316	3eqtrd	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to 1^{st} (D (c)) = J - e (Z)$
318	317	oveq2d	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to J - 1^{st} (D (c)) = J - (J - e (Z))$
319	298	adantr	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to J \in ℂ$
320		zsscn	$⊢ ℤ \subseteq ℂ$
321	107 320	sstri	$⊢ (0 \dots J) \subseteq ℂ$
322	321	a1i	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to (0 \dots J) \subseteq ℂ$
323		eleq1w	$⊢ c = e \to (c \in C (R \cup \{Z\}) (J) \leftrightarrow e \in C (R \cup \{Z\}) (J))$
324	323	anbi2d	$⊢ c = e \to ((φ \land c \in C (R \cup \{Z\}) (J)) \leftrightarrow (φ \land e \in C (R \cup \{Z\}) (J)))$
325		feq1	$⊢ c = e \to (c : R \cup \{Z\} ⟶ (0 \dots J) \leftrightarrow e : R \cup \{Z\} ⟶ (0 \dots J))$
326	324 325	imbi12d	$⊢ c = e \to (((φ \land c \in C (R \cup \{Z\}) (J)) \to c : R \cup \{Z\} ⟶ (0 \dots J)) \leftrightarrow ((φ \land e \in C (R \cup \{Z\}) (J)) \to e : R \cup \{Z\} ⟶ (0 \dots J)))$
327	326 48	chvarvv	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to e : R \cup \{Z\} ⟶ (0 \dots J)$
328	52	adantr	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to Z \in (R \cup \{Z\})$
329	327 328	ffvelcdmd	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to e (Z) \in (0 \dots J)$
330	322 329	sseldd	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to e (Z) \in ℂ$
331	319 330	nncand	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to J - (J - e (Z)) = e (Z)$
332	331	adantr	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to J - (J - e (Z)) = e (Z)$
333		eqidd	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to e (Z) = e (Z)$
334	318 332 333	3eqtrd	$⊢ ((φ \land e \in C (R \cup \{Z\}) (J)) \land D (c) = D (e)) \to J - 1^{st} (D (c)) = e (Z)$
335	334	adantlrl	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to J - 1^{st} (D (c)) = e (Z)$
336	303 310 335	3eqtrd	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to c (Z) = e (Z)$
337	336	adantr	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t = Z) \to c (Z) = e (Z)$
338		fveq2	$⊢ t = Z \to e (t) = e (Z)$
339	338	eqcomd	$⊢ t = Z \to e (Z) = e (t)$
340	339	adantl	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t = Z) \to e (Z) = e (t)$
341	297 337 340	3eqtrd	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t = Z) \to c (t) = e (t)$
342	341	adantlr	$⊢ ((((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in (R \cup \{Z\})) \land t = Z) \to c (t) = e (t)$
343	291 295 342	syl2anc	$⊢ ((((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to c (t) = e (t)$
344	290 343	pm2.61dan	$⊢ (((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \land t \in (R \cup \{Z\})) \to c (t) = e (t)$
345	344	ex	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to (t \in (R \cup \{Z\}) \to c (t) = e (t))$
346	248 345	ralrimi	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to \forall t \in (R \cup \{Z\}) c (t) = e (t)$
347	69	adantrr	$⊢ (φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \to c Fn (R \cup \{Z\})$
348	347	adantr	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to c Fn (R \cup \{Z\})$
349	327	ffnd	$⊢ (φ \land e \in C (R \cup \{Z\}) (J)) \to e Fn (R \cup \{Z\})$
350	349	adantrl	$⊢ (φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \to e Fn (R \cup \{Z\})$
351	350	adantr	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to e Fn (R \cup \{Z\})$
352		eqfnfv	$⊢ (c Fn (R \cup \{Z\}) \land e Fn (R \cup \{Z\})) \to (c = e \leftrightarrow \forall t \in (R \cup \{Z\}) c (t) = e (t))$
353	348 351 352	syl2anc	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to (c = e \leftrightarrow \forall t \in (R \cup \{Z\}) c (t) = e (t))$
354	346 353	mpbird	$⊢ ((φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \land D (c) = D (e)) \to c = e$
355	354	ex	$⊢ (φ \land (c \in C (R \cup \{Z\}) (J) \land e \in C (R \cup \{Z\}) (J))) \to (D (c) = D (e) \to c = e)$
356	355	ralrimivva	$⊢ φ \to \forall c \in C (R \cup \{Z\}) (J) \forall e \in C (R \cup \{Z\}) (J) (D (c) = D (e) \to c = e)$
357	243 356	jca	$⊢ φ \to (D : C (R \cup \{Z\}) (J) ⟶ ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \land \forall c \in C (R \cup \{Z\}) (J) \forall e \in C (R \cup \{Z\}) (J) (D (c) = D (e) \to c = e))$
358		dff13	$⊢ D : C (R \cup \{Z\}) (J) \underset{1-1}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \leftrightarrow (D : C (R \cup \{Z\}) (J) ⟶ ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \land \forall c \in C (R \cup \{Z\}) (J) \forall e \in C (R \cup \{Z\}) (J) (D (c) = D (e) \to c = e))$
359	357 358	sylibr	$⊢ φ \to D : C (R \cup \{Z\}) (J) \underset{1-1}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
360		eliun	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \leftrightarrow \exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k))$
361	360	biimpi	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \to \exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k))$
362	361	adantl	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k))$
363		nfv	$⊢ Ⅎ k φ$
364		nfcv	$⊢ \underline{Ⅎ} k p$
365		nfiu1	$⊢ \underline{Ⅎ} k ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
366	364 365	nfel	$⊢ Ⅎ k p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
367	363 366	nfan	$⊢ Ⅎ k (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)))$
368		nfv	$⊢ Ⅎ k (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
369		nfv	$⊢ Ⅎ t k \in (0 \dots J)$
370		nfcv	$⊢ \underline{Ⅎ} t p$
371		nfcv	$⊢ \underline{Ⅎ} t \{k\}$
372		nfcv	$⊢ \underline{Ⅎ} t R$
373	86 372	nffv	$⊢ \underline{Ⅎ} t C (R)$
374		nfcv	$⊢ \underline{Ⅎ} t k$
375	373 374	nffv	$⊢ \underline{Ⅎ} t C (R) (k)$
376	371 375	nfxp	$⊢ \underline{Ⅎ} t (\{k\} \times C (R) (k))$
377	370 376	nfel	$⊢ Ⅎ t p \in (\{k\} \times C (R) (k))$
378	74 369 377	nf3an	$⊢ Ⅎ t (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k)))$
379		0zd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to 0 \in ℤ$
380	10	adantr	$⊢ (φ \land t \in (R \cup \{Z\})) \to J \in ℤ$
381	380	3ad2antl1	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to J \in ℤ$
382		iftrue	$⊢ t \in R \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = 2^{nd} (p) (t)$
383	382	adantl	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land t \in R) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = 2^{nd} (p) (t)$
384		simp1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to φ$
385		simp2	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to k \in (0 \dots J)$
386		xp2nd	$⊢ p \in (\{k\} \times C (R) (k)) \to 2^{nd} (p) \in C (R) (k)$
387	386	3ad2ant3	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in C (R) (k)$
388	188	adantr	$⊢ (φ \land k \in (0 \dots J)) \to C (R) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\})$
389		oveq2	$⊢ n = k \to (0 \dots n) = (0 \dots k)$
390	389	oveq1d	$⊢ n = k \to {(0 \dots n)}^{R} = {(0 \dots k)}^{R}$
391		rabeq	$⊢ {(0 \dots n)}^{R} = {(0 \dots k)}^{R} \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = n\}$
392	390 391	syl	$⊢ n = k \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = n\}$
393		eqeq2	$⊢ n = k \to (\sum_{t \in R} c (t) = n \leftrightarrow \sum_{t \in R} c (t) = k)$
394	393	rabbidv	$⊢ n = k \to \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
395	392 394	eqtrd	$⊢ n = k \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
396	395	adantl	$⊢ ((φ \land k \in (0 \dots J)) \land n = k) \to \{c \in ({(0 \dots n)}^{R}) \| \sum_{t \in R} c (t) = n\} = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
397		elfznn0	$⊢ k \in (0 \dots J) \to k \in ℕ_{0}$
398	397	adantl	$⊢ (φ \land k \in (0 \dots J)) \to k \in ℕ_{0}$
399		ovex	$⊢ {(0 \dots k)}^{R} \in V$
400	399	rabex	$⊢ \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \in V$
401	400	a1i	$⊢ (φ \land k \in (0 \dots J)) \to \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \in V$
402	388 396 398 401	fvmptd	$⊢ (φ \land k \in (0 \dots J)) \to C (R) (k) = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
403	402	3adant3	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to C (R) (k) = \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
404	387 403	eleqtrd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}$
405		elrabi	$⊢ 2^{nd} (p) \in \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \to 2^{nd} (p) \in ({(0 \dots k)}^{R})$
406	405	3ad2ant3	$⊢ (φ \land k \in (0 \dots J) \land 2^{nd} (p) \in \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\}) \to 2^{nd} (p) \in ({(0 \dots k)}^{R})$
407	384 385 404 406	syl3anc	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) \in ({(0 \dots k)}^{R})$
408		elmapi	$⊢ 2^{nd} (p) \in ({(0 \dots k)}^{R}) \to 2^{nd} (p) : R ⟶ (0 \dots k)$
409	407 408	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) : R ⟶ (0 \dots k)$
410	409	adantr	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to 2^{nd} (p) : R ⟶ (0 \dots k)$
411	410	ffvelcdmda	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land t \in R) \to 2^{nd} (p) (t) \in (0 \dots k)$
412	411	elfzelzd	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land t \in R) \to 2^{nd} (p) (t) \in ℤ$
413	383 412	eqeltrd	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land t \in R) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \in ℤ$
414		simpl	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\}))$
415	294	adantll	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to t = Z$
416		simpr	$⊢ (φ \land t = Z) \to t = Z$
417	6	adantr	$⊢ (φ \land t = Z) \to \neg Z \in R$
418	416 417	eqneltrd	$⊢ (φ \land t = Z) \to \neg t \in R$
419	418	iffalsed	$⊢ (φ \land t = Z) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = J - 1^{st} (p)$
420	419	3ad2antl1	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = J - 1^{st} (p)$
421	10	adantr	$⊢ (φ \land t = Z) \to J \in ℤ$
422	421	3ad2antl1	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to J \in ℤ$
423		xp1st	$⊢ p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in \{k\}$
424		elsni	$⊢ 1^{st} (p) \in \{k\} \to 1^{st} (p) = k$
425	423 424	syl	$⊢ p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) = k$
426	425	adantl	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) = k$
427	107	sseli	$⊢ k \in (0 \dots J) \to k \in ℤ$
428	427	adantr	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to k \in ℤ$
429	426 428	eqeltrd	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in ℤ$
430	429	3adant1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in ℤ$
431	430	adantr	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to 1^{st} (p) \in ℤ$
432	422 431	zsubcld	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to J - 1^{st} (p) \in ℤ$
433	420 432	eqeltrd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \in ℤ$
434	433	adantlr	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land t = Z) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \in ℤ$
435	414 415 434	syl2anc	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \in ℤ$
436	413 435	pm2.61dan	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \in ℤ$
437	409	ffvelcdmda	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t) \in (0 \dots k)$
438		elfzle1	$⊢ 2^{nd} (p) (t) \in (0 \dots k) \to 0 \leq 2^{nd} (p) (t)$
439	437 438	syl	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to 0 \leq 2^{nd} (p) (t)$
440	382	eqcomd	$⊢ t \in R \to 2^{nd} (p) (t) = if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
441	440	adantl	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t) = if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
442	439 441	breqtrd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to 0 \leq if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
443	442	adantlr	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land t \in R) \to 0 \leq if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
444		simpll	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k)))$
445		elfzle2	$⊢ k \in (0 \dots J) \to k \leq J$
446		elfzel2	$⊢ k \in (0 \dots J) \to J \in ℤ$
447	446	zred	$⊢ k \in (0 \dots J) \to J \in ℝ$
448	109	sseli	$⊢ k \in (0 \dots J) \to k \in ℝ$
449	447 448	subge0d	$⊢ k \in (0 \dots J) \to (0 \leq J - k \leftrightarrow k \leq J)$
450	445 449	mpbird	$⊢ k \in (0 \dots J) \to 0 \leq J - k$
451	450	adantr	$⊢ (k \in (0 \dots J) \land t = Z) \to 0 \leq J - k$
452	451	3ad2antl2	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to 0 \leq J - k$
453	384 418	sylan	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to \neg t \in R$
454	453	iffalsed	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = J - 1^{st} (p)$
455	426	3adant1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) = k$
456	455	oveq2d	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to J - 1^{st} (p) = J - k$
457	456	adantr	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to J - 1^{st} (p) = J - k$
458	454 457	eqtr2d	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to J - k = if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
459	452 458	breqtrd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to 0 \leq if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
460	444 415 459	syl2anc	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to 0 \leq if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
461	443 460	pm2.61dan	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to 0 \leq if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
462		simpl2	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to k \in (0 \dots J)$
463		fzssz	$⊢ (0 \dots k) \subseteq ℤ$
464	463	sseli	$⊢ 2^{nd} (p) (t) \in (0 \dots k) \to 2^{nd} (p) (t) \in ℤ$
465	464	zred	$⊢ 2^{nd} (p) (t) \in (0 \dots k) \to 2^{nd} (p) (t) \in ℝ$
466	465	adantr	$⊢ (2^{nd} (p) (t) \in (0 \dots k) \land k \in (0 \dots J)) \to 2^{nd} (p) (t) \in ℝ$
467	448	adantl	$⊢ (2^{nd} (p) (t) \in (0 \dots k) \land k \in (0 \dots J)) \to k \in ℝ$
468	447	adantl	$⊢ (2^{nd} (p) (t) \in (0 \dots k) \land k \in (0 \dots J)) \to J \in ℝ$
469		elfzle2	$⊢ 2^{nd} (p) (t) \in (0 \dots k) \to 2^{nd} (p) (t) \leq k$
470	469	adantr	$⊢ (2^{nd} (p) (t) \in (0 \dots k) \land k \in (0 \dots J)) \to 2^{nd} (p) (t) \leq k$
471	445	adantl	$⊢ (2^{nd} (p) (t) \in (0 \dots k) \land k \in (0 \dots J)) \to k \leq J$
472	466 467 468 470 471	letrd	$⊢ (2^{nd} (p) (t) \in (0 \dots k) \land k \in (0 \dots J)) \to 2^{nd} (p) (t) \leq J$
473	437 462 472	syl2anc	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t) \leq J$
474	473	adantlr	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land t \in R) \to 2^{nd} (p) (t) \leq J$
475	383 474	eqbrtrd	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land t \in R) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \leq J$
476	458	eqcomd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = J - k$
477	398	nn0ge0d	$⊢ (φ \land k \in (0 \dots J)) \to 0 \leq k$
478	447	adantl	$⊢ (φ \land k \in (0 \dots J)) \to J \in ℝ$
479	448	adantl	$⊢ (φ \land k \in (0 \dots J)) \to k \in ℝ$
480	478 479	subge02d	$⊢ (φ \land k \in (0 \dots J)) \to (0 \leq k \leftrightarrow J - k \leq J)$
481	477 480	mpbid	$⊢ (φ \land k \in (0 \dots J)) \to J - k \leq J$
482	481	adantr	$⊢ ((φ \land k \in (0 \dots J)) \land t = Z) \to J - k \leq J$
483	482	3adantl3	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to J - k \leq J$
484	476 483	eqbrtrd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t = Z) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \leq J$
485	444 415 484	syl2anc	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land \neg t \in R) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \leq J$
486	475 485	pm2.61dan	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \leq J$
487	379 381 436 461 486	elfzd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \in (0 \dots J)$
488		eqid	$⊢ (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))$
489	378 487 488	fmptdf	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) : R \cup \{Z\} ⟶ (0 \dots J)$
490		ovexd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (0 \dots J) \in V$
491	384 21	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to R \cup \{Z\} \in V$
492	490 491	elmapd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to ((t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in ({(0 \dots J)}^{(R \cup \{Z\})}) \leftrightarrow (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) : R \cup \{Z\} ⟶ (0 \dots J))$
493	489 492	mpbird	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in ({(0 \dots J)}^{(R \cup \{Z\})})$
494		eqidd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)))$
495		eleq1w	$⊢ r = t \to (r \in R \leftrightarrow t \in R)$
496		fveq2	$⊢ r = t \to 2^{nd} (p) (r) = 2^{nd} (p) (t)$
497	495 496	ifbieq1d	$⊢ r = t \to if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)) = if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
498	497	adantl	$⊢ (((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \land r = t) \to if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)) = if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
499		simpr	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to t \in (R \cup \{Z\})$
500	494 498 499 436	fvmptd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in (R \cup \{Z\})) \to (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t) = if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
501	500	ex	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (t \in (R \cup \{Z\}) \to (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t) = if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))$
502	378 501	ralrimi	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \forall t \in (R \cup \{Z\}) (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t) = if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
503	502	sumeq2d	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \sum_{t \in R \cup \{Z\}} (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t) = \sum_{t \in R \cup \{Z\}} if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))$
504		nfcv	$⊢ \underline{Ⅎ} t if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p))$
505	384 105	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to R \in Fin$
506	384 5	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to Z \in T$
507	384 6	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \neg Z \in R$
508	382	adantl	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = 2^{nd} (p) (t)$
509	437	elfzelzd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t) \in ℤ$
510	509	zcnd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to 2^{nd} (p) (t) \in ℂ$
511	508 510	eqeltrd	$⊢ ((φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \land t \in R) \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) \in ℂ$
512		eleq1	$⊢ t = Z \to (t \in R \leftrightarrow Z \in R)$
513		fveq2	$⊢ t = Z \to 2^{nd} (p) (t) = 2^{nd} (p) (Z)$
514	512 513	ifbieq1d	$⊢ t = Z \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p))$
515	6	adantr	$⊢ (φ \land p \in (\{k\} \times C (R) (k))) \to \neg Z \in R$
516	515	iffalsed	$⊢ (φ \land p \in (\{k\} \times C (R) (k))) \to if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p)) = J - 1^{st} (p)$
517	516	3adant2	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p)) = J - 1^{st} (p)$
518	10	3ad2ant1	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to J \in ℤ$
519	518 430	zsubcld	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in ℤ$
520	519	zcnd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to J - 1^{st} (p) \in ℂ$
521	517 520	eqeltrd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p)) \in ℂ$
522	378 504 505 506 507 511 514 521	fsumsplitsn	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \sum_{t \in R \cup \{Z\}} if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = \sum_{t \in R} if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) + if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p))$
523	382	a1i	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (t \in R \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = 2^{nd} (p) (t))$
524	378 523	ralrimi	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \forall t \in R if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = 2^{nd} (p) (t)$
525	524	sumeq2d	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \sum_{t \in R} if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = \sum_{t \in R} 2^{nd} (p) (t)$
526		eqidd	$⊢ c = 2^{nd} (p) \to R = R$
527		simpl	$⊢ (c = 2^{nd} (p) \land t \in R) \to c = 2^{nd} (p)$
528	527	fveq1d	$⊢ (c = 2^{nd} (p) \land t \in R) \to c (t) = 2^{nd} (p) (t)$
529	526 528	sumeq12rdv	$⊢ c = 2^{nd} (p) \to \sum_{t \in R} c (t) = \sum_{t \in R} 2^{nd} (p) (t)$
530	529	eqeq1d	$⊢ c = 2^{nd} (p) \to (\sum_{t \in R} c (t) = k \leftrightarrow \sum_{t \in R} 2^{nd} (p) (t) = k)$
531	530	elrab	$⊢ 2^{nd} (p) \in \{c \in ({(0 \dots k)}^{R}) \| \sum_{t \in R} c (t) = k\} \leftrightarrow (2^{nd} (p) \in ({(0 \dots k)}^{R}) \land \sum_{t \in R} 2^{nd} (p) (t) = k)$
532	404 531	sylib	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (2^{nd} (p) \in ({(0 \dots k)}^{R}) \land \sum_{t \in R} 2^{nd} (p) (t) = k)$
533	532	simprd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \sum_{t \in R} 2^{nd} (p) (t) = k$
534	525 533	eqtrd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \sum_{t \in R} if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = k$
535	507	iffalsed	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p)) = J - 1^{st} (p)$
536	535 456	eqtrd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p)) = J - k$
537	534 536	oveq12d	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \sum_{t \in R} if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) + if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p)) = k + J - k$
538	321	sseli	$⊢ k \in (0 \dots J) \to k \in ℂ$
539	538	3ad2ant2	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to k \in ℂ$
540	384 298	syl	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to J \in ℂ$
541	539 540	pncan3d	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to k + J - k = J$
542	537 541	eqtrd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \sum_{t \in R} if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) + if (Z \in R, 2^{nd} (p) (Z), J - 1^{st} (p)) = J$
543	503 522 542	3eqtrd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to \sum_{t \in R \cup \{Z\}} (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t) = J$
544	493 543	jca	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to ((t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in ({(0 \dots J)}^{(R \cup \{Z\})}) \land \sum_{t \in R \cup \{Z\}} (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t) = J)$
545		eleq1w	$⊢ t = r \to (t \in R \leftrightarrow r \in R)$
546		fveq2	$⊢ t = r \to 2^{nd} (p) (t) = 2^{nd} (p) (r)$
547	545 546	ifbieq1d	$⊢ t = r \to if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)) = if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))$
548	547	cbvmptv	$⊢ (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)))$
549	548	eqeq2i	$⊢ c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \leftrightarrow c = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)))$
550	549	biimpi	$⊢ c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \to c = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)))$
551		fveq1	$⊢ c = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) \to c (t) = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t)$
552	551	sumeq2sdv	$⊢ c = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) \to \sum_{t \in R \cup \{Z\}} c (t) = \sum_{t \in R \cup \{Z\}} (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t)$
553	550 552	syl	$⊢ c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \to \sum_{t \in R \cup \{Z\}} c (t) = \sum_{t \in R \cup \{Z\}} (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t)$
554	553	eqeq1d	$⊢ c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \to (\sum_{t \in R \cup \{Z\}} c (t) = J \leftrightarrow \sum_{t \in R \cup \{Z\}} (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t) = J)$
555	554	elrab	$⊢ (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} \leftrightarrow ((t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in ({(0 \dots J)}^{(R \cup \{Z\})}) \land \sum_{t \in R \cup \{Z\}} (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p))) (t) = J)$
556	544 555	sylibr	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
557	556	3exp	$⊢ φ \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}))$
558	557	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}))$
559	367 368 558	rexlimd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k)) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\})$
560	362 559	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\}$
561	40	eqcomd	$⊢ φ \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} = C (R \cup \{Z\}) (J)$
562	561	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \{c \in ({(0 \dots J)}^{(R \cup \{Z\})}) \| \sum_{t \in R \cup \{Z\}} c (t) = J\} = C (R \cup \{Z\}) (J)$
563	560 562	eleqtrd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in C (R \cup \{Z\}) (J)$
564	3	a1i	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to D = (c \in C (R \cup \{Z\}) (J) ⟼ ⟨J - c (Z), {c ↾}_{R}⟩)$
565		simpr	$⊢ (φ \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))$
566	548	a1i	$⊢ (φ \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)))$
567	565 566	eqtrd	$⊢ (φ \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to c = (r \in (R \cup \{Z\}) ⟼ if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)))$
568		simpr	$⊢ (φ \land r = Z) \to r = Z$
569	6	adantr	$⊢ (φ \land r = Z) \to \neg Z \in R$
570	568 569	eqneltrd	$⊢ (φ \land r = Z) \to \neg r \in R$
571	570	iffalsed	$⊢ (φ \land r = Z) \to if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)) = J - 1^{st} (p)$
572	571	adantlr	$⊢ ((φ \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \land r = Z) \to if (r \in R, 2^{nd} (p) (r), J - 1^{st} (p)) = J - 1^{st} (p)$
573	52	adantr	$⊢ (φ \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to Z \in (R \cup \{Z\})$
574		ovexd	$⊢ (φ \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to J - 1^{st} (p) \in V$
575	567 572 573 574	fvmptd	$⊢ (φ \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to c (Z) = J - 1^{st} (p)$
576	575	oveq2d	$⊢ (φ \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to J - c (Z) = J - (J - 1^{st} (p))$
577	576	adantlr	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to J - c (Z) = J - (J - 1^{st} (p))$
578	298	ad2antrr	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to J \in ℂ$
579		nfv	$⊢ Ⅎ k 1^{st} (p) \in (0 \dots J)$
580		simpl	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to k \in (0 \dots J)$
581		simpr	$⊢ (k \in (0 \dots J) \land 1^{st} (p) = k) \to 1^{st} (p) = k$
582		simpl	$⊢ (k \in (0 \dots J) \land 1^{st} (p) = k) \to k \in (0 \dots J)$
583	581 582	eqeltrd	$⊢ (k \in (0 \dots J) \land 1^{st} (p) = k) \to 1^{st} (p) \in (0 \dots J)$
584	580 426 583	syl2anc	$⊢ (k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 1^{st} (p) \in (0 \dots J)$
585	584	ex	$⊢ k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J))$
586	585	a1i	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J)))$
587	366 579 586	rexlimd	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \to (\exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J))$
588	361 587	mpd	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \to 1^{st} (p) \in (0 \dots J)$
589	588	elfzelzd	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \to 1^{st} (p) \in ℤ$
590	589	zcnd	$⊢ p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \to 1^{st} (p) \in ℂ$
591	590	ad2antlr	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to 1^{st} (p) \in ℂ$
592	578 591	nncand	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to J - (J - 1^{st} (p)) = 1^{st} (p)$
593	577 592	eqtrd	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to J - c (Z) = 1^{st} (p)$
594		reseq1	$⊢ c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \to {c ↾}_{R} = {(t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) ↾}_{R}$
595	594	adantl	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to {c ↾}_{R} = {(t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) ↾}_{R}$
596	70	a1i	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to R \subseteq R \cup \{Z\}$
597	596	resmptd	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to {(t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) ↾}_{R} = (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))$
598		nfv	$⊢ Ⅎ k (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = 2^{nd} (p)$
599	382	mpteq2ia	$⊢ (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = (t \in R ⟼ 2^{nd} (p) (t))$
600	599	a1i	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = (t \in R ⟼ 2^{nd} (p) (t))$
601	409	feqmptd	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to 2^{nd} (p) = (t \in R ⟼ 2^{nd} (p) (t))$
602	600 601	eqtr4d	$⊢ (φ \land k \in (0 \dots J) \land p \in (\{k\} \times C (R) (k))) \to (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = 2^{nd} (p)$
603	602	3exp	$⊢ φ \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = 2^{nd} (p)))$
604	603	adantr	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = 2^{nd} (p)))$
605	367 598 604	rexlimd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k)) \to (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = 2^{nd} (p))$
606	362 605	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = 2^{nd} (p)$
607	606	adantr	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to (t \in R ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) = 2^{nd} (p)$
608	595 597 607	3eqtrd	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to {c ↾}_{R} = 2^{nd} (p)$
609	593 608	opeq12d	$⊢ ((φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \land c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) \to ⟨J - c (Z), {c ↾}_{R}⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩$
610		opex	$⊢ ⟨1^{st} (p), 2^{nd} (p)⟩ \in V$
611	610	a1i	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to ⟨1^{st} (p), 2^{nd} (p)⟩ \in V$
612	564 609 563 611	fvmptd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to D ((t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p)))) = ⟨1^{st} (p), 2^{nd} (p)⟩$
613		nfv	$⊢ Ⅎ k ⟨1^{st} (p), 2^{nd} (p)⟩ = p$
614		1st2nd2	$⊢ p \in (\{k\} \times C (R) (k)) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
615	614	eqcomd	$⊢ p \in (\{k\} \times C (R) (k)) \to ⟨1^{st} (p), 2^{nd} (p)⟩ = p$
616	615	a1i	$⊢ k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to ⟨1^{st} (p), 2^{nd} (p)⟩ = p)$
617	616	a1i	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (k \in (0 \dots J) \to (p \in (\{k\} \times C (R) (k)) \to ⟨1^{st} (p), 2^{nd} (p)⟩ = p))$
618	367 613 617	rexlimd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to (\exists k \in (0 \dots J) p \in (\{k\} \times C (R) (k)) \to ⟨1^{st} (p), 2^{nd} (p)⟩ = p)$
619	362 618	mpd	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to ⟨1^{st} (p), 2^{nd} (p)⟩ = p$
620	612 619	eqtr2d	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to p = D ((t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))))$
621		fveq2	$⊢ c = (t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \to D (c) = D ((t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))))$
622	621	rspceeqv	$⊢ ((t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))) \in C (R \cup \{Z\}) (J) \land p = D ((t \in (R \cup \{Z\}) ⟼ if (t \in R, 2^{nd} (p) (t), J - 1^{st} (p))))) \to \exists c \in C (R \cup \{Z\}) (J) p = D (c)$
623	563 620 622	syl2anc	$⊢ (φ \land p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))) \to \exists c \in C (R \cup \{Z\}) (J) p = D (c)$
624	623	ralrimiva	$⊢ φ \to \forall p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \exists c \in C (R \cup \{Z\}) (J) p = D (c)$
625	243 624	jca	$⊢ φ \to (D : C (R \cup \{Z\}) (J) ⟶ ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \land \forall p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \exists c \in C (R \cup \{Z\}) (J) p = D (c))$
626		dffo3	$⊢ D : C (R \cup \{Z\}) (J) \underset{onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \leftrightarrow (D : C (R \cup \{Z\}) (J) ⟶ ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \land \forall p \in ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \exists c \in C (R \cup \{Z\}) (J) p = D (c))$
627	625 626	sylibr	$⊢ φ \to D : C (R \cup \{Z\}) (J) \underset{onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$
628	359 627	jca	$⊢ φ \to (D : C (R \cup \{Z\}) (J) \underset{1-1}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \land D : C (R \cup \{Z\}) (J) \underset{onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)))$
629		df-f1o	$⊢ D : C (R \cup \{Z\}) (J) \underset{1-1 onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \leftrightarrow (D : C (R \cup \{Z\}) (J) \underset{1-1}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)) \land D : C (R \cup \{Z\}) (J) \underset{onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k)))$
630	628 629	sylibr	$⊢ φ \to D : C (R \cup \{Z\}) (J) \underset{1-1 onto}{⟶} ⋃_{k = 0}^{J} (\{k\} \times C (R) (k))$

Metamath Proof Explorer

Theorem dvnprodlem1

Proof