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