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