dvnprodlem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvnprodlem1		Structured version Visualization version GIF version

Theorem dvnprodlem1 43487

Description: 𝐷 is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

**Hypotheses**
Ref	Expression
dvnprodlem1.c	⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
dvnprodlem1.j	⊢ (𝜑 → 𝐽 ∈ ℕ₀)
dvnprodlem1.d	⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
dvnprodlem1.t	⊢ (𝜑 → 𝑇 ∈ Fin)
dvnprodlem1.z	⊢ (𝜑 → 𝑍 ∈ 𝑇)
dvnprodlem1.zr	⊢ (𝜑 → ¬ 𝑍 ∈ 𝑅)
dvnprodlem1.rzt	⊢ (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)

**Assertion**
Ref	Expression
dvnprodlem1	⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))

Distinct variable groups: 𝐶,𝑐,𝑘 𝐷,𝑐,𝑡 𝐽,𝑐,𝑘,𝑛,𝑡 𝑅,𝑐,𝑘,𝑛,𝑡 𝑅,𝑠,𝑐,𝑛,𝑡 𝑡,𝑇,𝑠 𝑍,𝑐,𝑘,𝑛,𝑡 𝑍,𝑠 𝜑,𝑐,𝑛,𝑡,𝑘 𝜑,𝑠 Allowed substitution hints: 𝐶(𝑡,𝑛,𝑠) 𝐷(𝑘,𝑛,𝑠) 𝑇(𝑘,𝑛,𝑐) 𝐽(𝑠)

Proof of Theorem dvnprodlem1 Dummy variables 𝑑 𝑒 𝑚 𝑝 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2739	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
2		0zd 12331	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3		dvnprodlem1.j	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
4	3	nn0zd 12424	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℤ)
5	4	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6		dvnprodlem1.c	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
7		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})))
8		rabeq 3418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
9	7, 8	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
10		sumeq1 15400	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
11	10	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛))
12	11	rabbidv 3414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
13	9, 12	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
14	13	mpteq2dv 5176	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
15		dvnprodlem1.rzt	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
16		dvnprodlem1.t	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ Fin)
17		ssexg 5247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∪ {𝑍}) ⊆ 𝑇 ∧ 𝑇 ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ V)
18	15, 16, 17	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
19		elpwg 4536	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
21	15, 20	mpbird 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
22		nn0ex 12239	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ₀ ∈ V
23	22	mptex 7099	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V
24	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V)
25	6, 14, 21, 24	fvmptd3 6898	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
26		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
27	26	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝐽 → ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
28		rabeq 3418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
30		eqeq2 2750	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
31	30	rabbidv 3414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
32	29, 31	eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
33	32	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
34		ovex 7308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∈ V
35	34	rabex 5256	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V
36	35	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V)
37	25, 33, 3, 36	fvmptd 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
38		ssrab2 4013	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍}))
39	38	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
40	37, 39	eqsstrd 3959	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
41	40	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
42		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
43	41, 42	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
44		elmapi 8637	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
45	43, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
46		dvnprodlem1.z	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ 𝑇)
47		snidg 4595	. . . . . . . . . . . . . . . . 17 ⊢ (𝑍 ∈ 𝑇 → 𝑍 ∈ {𝑍})
48	46, 47	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
49		elun2 4111	. . . . . . . . . . . . . . . 16 ⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
50	48, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑍 ∈ (𝑅 ∪ {𝑍}))
51	50	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
52	45, 51	ffvelrnd 6962	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ (0...𝐽))
53	52	elfzelzd 13257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℤ)
54	5, 53	zsubcld 12431	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
55		elfzle2 13260	. . . . . . . . . . . . 13 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → (𝑐‘𝑍) ≤ 𝐽)
56	52, 55	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ≤ 𝐽)
57	5	zred 12426	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
58	53	zred 12426	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℝ)
59	57, 58	subge0d 11565	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐‘𝑍)) ↔ (𝑐‘𝑍) ≤ 𝐽))
60	56, 59	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐‘𝑍)))
61		elfzle1 13259	. . . . . . . . . . . . 13 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑍))
62	52, 61	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐‘𝑍))
63	57, 58	subge02d 11567	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐‘𝑍) ↔ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽))
64	62, 63	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)
65	2, 5, 54, 60, 64	elfzd 13247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽))
66		elmapfn 8653	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
67	43, 66	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
68		ssun1 4106	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 ⊆ (𝑅 ∪ {𝑍})
69	68	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
70		fnssres 6555	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑅 ⊆ (𝑅 ∪ {𝑍})) → (𝑐 ↾ 𝑅) Fn 𝑅)
71	67, 69, 70	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) Fn 𝑅)
72		nfv 1917	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝜑
73		nfcv 2907	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡𝑐
74		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡𝒫 𝑇
75		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡ℕ₀
76		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡𝑠
77	76	nfsum1 15401	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡)
78		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡𝑛
79	77, 78	nfeq 2920	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛
80		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡((0...𝑛) ↑_m 𝑠)
81	79, 80	nfrabw 3318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡{𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}
82	75, 81	nfmpt 5181	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
83	74, 82	nfmpt 5181	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
84	6, 83	nfcxfr 2905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡𝐶
85		nfcv 2907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡(𝑅 ∪ {𝑍})
86	84, 85	nffv 6784	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝐶‘(𝑅 ∪ {𝑍}))
87		nfcv 2907	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐽
88	86, 87	nffv 6784	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
89	73, 88	nfel 2921	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
90	72, 89	nfan 1902	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
91		fvres 6793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
92	91	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
93	2	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ∈ ℤ)
94	54	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
95	45	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
96	69	sselda 3921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
97	95, 96	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...𝐽))
98	97	elfzelzd 13257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ ℤ)
99		elfzle1 13259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐‘𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑡))
100	97, 99	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ≤ (𝑐‘𝑡))
101	15	unssad 4121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ⊆ 𝑇)
102		ssfi 8956	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 ∈ Fin ∧ 𝑅 ⊆ 𝑇) → 𝑅 ∈ Fin)
103	16, 101, 102	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑅 ∈ Fin)
104	103	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑅 ∈ Fin)
105		fzssz 13258	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0...𝐽) ⊆ ℤ
106		zssre 12326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ℤ ⊆ ℝ
107	105, 106	sstri 3930	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0...𝐽) ⊆ ℝ
108	107	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (0...𝐽) ⊆ ℝ)
109	45	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
110	69	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
111	109, 110	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ (0...𝐽))
112	108, 111	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
113	112	adantlr 712	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
114		elfzle1 13259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐‘𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑟))
115	111, 114	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
116	115	adantlr 712	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
117		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟 = 𝑡 → (𝑐‘𝑟) = (𝑐‘𝑡))
118		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ 𝑅)
119	104, 113, 116, 117, 118	fsumge1 15509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
120	103	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
121	112	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℂ)
122	120, 121	fsumcl 15445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) ∈ ℂ)
123	58	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℂ)
124	122, 123	pncand 11333	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) − (𝑐‘𝑍)) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
125		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑟(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
126		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑟(𝑐‘𝑍)
127	46	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ 𝑇)
128		dvnprodlem1.zr	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑅)
129	128	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍 ∈ 𝑅)
130		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑟 = 𝑍 → (𝑐‘𝑟) = (𝑐‘𝑍))
131	125, 126, 120, 127, 129, 121, 130, 123	fsumsplitsn 15456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)))
132	131	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟))
133	117	cbvsumv 15408	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡)
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
135	37	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
136	42, 135	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
137		rabid 3310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
138	136, 137	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
139	138	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽)
140	134, 139	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = 𝐽)
141	132, 140	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = 𝐽)
142	141	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) − (𝑐‘𝑍)) = (𝐽 − (𝑐‘𝑍)))
143	124, 142	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
144	143	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
145	119, 144	breqtrd 5100	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))
146	93, 94, 98, 100, 145	elfzd 13247	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
147	92, 146	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
148	147	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
149	90, 148	ralrimi 3141	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
150	71, 149	jca 512	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
151		ffnfv 6992	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))) ↔ ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
152	150, 151	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))))
153		ovexd 7310	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐‘𝑍))) ∈ V)
154	16, 101	ssexd 5248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ V)
155	154	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ V)
156	153, 155	elmapd 8629	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ↔ (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍)))))
157	152, 156	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅))
158	91	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡)))
159	90, 158	ralrimi 3141	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
160	159	sumeq2d 15414	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
161	117	cbvsumv 15408	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡)
162	161	eqcomi 2747	. . . . . . . . . . . . . . 15 ⊢ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟)
163	162	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
164	143	idi 1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
165	160, 163, 164	3eqtrd 2782	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍)))
166	157, 165	jca 512	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
167		eqidd 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → 𝑅 = 𝑅)
168		simpl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → 𝑒 = (𝑐 ↾ 𝑅))
169	168	fveq1d 6776	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → (𝑒‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
170	167, 169	sumeq12rdv 15419	. . . . . . . . . . . . . 14 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡))
171	170	eqeq1d 2740	. . . . . . . . . . . . 13 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍)) ↔ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
172	171	elrab 3624	. . . . . . . . . . . 12 ⊢ ((𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ↔ ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
173	166, 172	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
174		oveq2 7283	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑅 → ((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m 𝑅))
175		rabeq 3418	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
176	174, 175	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
177		sumeq1 15400	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑅 → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
178	177	eqeq1d 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑅 → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛))
179	178	rabbidv 3414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
180	176, 179	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
181	180	mpteq2dv 5176	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑅 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
182		elpwg 4536	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇 ↔ 𝑅 ⊆ 𝑇))
183	154, 182	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ∈ 𝒫 𝑇 ↔ 𝑅 ⊆ 𝑇))
184	101, 183	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ 𝒫 𝑇)
185	22	mptex 7099	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V
186	185	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V)
187	6, 181, 184, 186	fvmptd3 6898	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
188	187	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
189		oveq2 7283	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
190	189	oveq1d 7290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((0...𝑛) ↑_m 𝑅) = ((0...𝑚) ↑_m 𝑅))
191		rabeq 3418	. . . . . . . . . . . . . . . . . 18 ⊢ (((0...𝑛) ↑_m 𝑅) = ((0...𝑚) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
192	190, 191	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
193		eqeq2 2750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚))
194	193	rabbidv 3414	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
195	192, 194	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
196	195	cbvmptv 5187	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
197	196	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
198	188, 197	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
199		fveq1 6773	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑡) = (𝑒‘𝑡))
200	199	sumeq2sdv 15416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑒 → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑒‘𝑡))
201	200	eqeq1d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚))
202	201	cbvrabv 3426	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚}
203	202	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
204		oveq2 7283	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐‘𝑍))))
205	204	oveq1d 7290	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → ((0...𝑚) ↑_m 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅))
206		rabeq 3418	. . . . . . . . . . . . . . . 16 ⊢ (((0...𝑚) ↑_m 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) → {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
207	205, 206	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
208		eqeq2 2750	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))))
209	208	rabbidv 3414	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
210	203, 207, 209	3eqtrd 2782	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
211	210	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑚 = (𝐽 − (𝑐‘𝑍))) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
212	54, 60	jca 512	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
213		elnn0z 12332	. . . . . . . . . . . . . 14 ⊢ ((𝐽 − (𝑐‘𝑍)) ∈ ℕ₀ ↔ ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
214	212, 213	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℕ₀)
215		ovex 7308	. . . . . . . . . . . . . . 15 ⊢ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∈ V
216	215	rabex 5256	. . . . . . . . . . . . . 14 ⊢ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V
217	216	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V)
218	198, 211, 214, 217	fvmptd 6882	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
219	218	eqcomd 2744	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
220	173, 219	eleqtrd 2841	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
221	65, 220	jca 512	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
222	1, 221	jca 512	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
223		ovexd 7310	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ V)
224		vex 3436	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
225	224	resex 5939	. . . . . . . . . 10 ⊢ (𝑐 ↾ 𝑅) ∈ V
226	225	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ V)
227		opeq12 4806	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
228	227	eqeq2d 2749	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
229		eleq1 2826	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
230	229	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
231		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → 𝑑 = (𝑐 ↾ 𝑅))
232		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
233	232	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
234	231, 233	eleq12d 2833	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑑 ∈ ((𝐶‘𝑅)‘𝑘) ↔ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
235	230, 234	anbi12d 631	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
236	228, 235	anbi12d 631	. . . . . . . . . 10 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))))
237	236	spc2egv 3538	. . . . . . . . 9 ⊢ (((𝐽 − (𝑐‘𝑍)) ∈ V ∧ (𝑐 ↾ 𝑅) ∈ V) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
238	223, 226, 237	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
239	222, 238	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
240		eliunxp 5746	. . . . . . 7 ⊢ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
241	239, 240	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
242		dvnprodlem1.d	. . . . . 6 ⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
243	241, 242	fmptd 6988	. . . . 5 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
244	88	nfcri 2894	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
245	89, 244	nfan 1902	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
246	72, 245	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
247		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝐷‘𝑐) = (𝐷‘𝑒)
248	246, 247	nfan 1902	. . . . . . . . 9 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒))
249	92	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
250	249	adantlrr 718	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
251	250	adantlr 712	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
252	242	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
253		opex 5379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V
254	253	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V)
255	252, 254	fvmpt2d 6888	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
256	255	fveq2d 6778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
257	256	fveq1d 6776	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡))
258		ovex 7308	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 − (𝑐‘𝑍)) ∈ V
259	258, 225	op2nd 7840	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝑐 ↾ 𝑅)
260	259	fveq1i 6775	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡)
261	260	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
262	257, 261	eqtr2d 2779	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
263	262	adantrr 714	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
264	263	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
265		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = (𝐷‘𝑒))
266		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑍) = (𝑒‘𝑍))
267	266	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝑒‘𝑍)))
268		reseq1 5885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (𝑐 ↾ 𝑅) = (𝑒 ↾ 𝑅))
269	267, 268	opeq12d 4812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
270		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
271		opex 5379	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V
272	271	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V)
273	242, 269, 270, 272	fvmptd3 6898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
274	273	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
275	265, 274	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
276	275	fveq2d 6778	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
277	276	adantlrl 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
278	277	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
279		ovex 7308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 − (𝑒‘𝑍)) ∈ V
280		vex 3436	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑒 ∈ V
281	280	resex 5939	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ↾ 𝑅) ∈ V
282	279, 281	op2nd 7840	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅)
283	282	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅))
284	278, 283	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘(𝐷‘𝑐)) = (𝑒 ↾ 𝑅))
285	284	fveq1d 6776	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = ((𝑒 ↾ 𝑅)‘𝑡))
286		fvres 6793	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝑅 → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
287	286	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
288	285, 287	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = (𝑒‘𝑡))
289	251, 264, 288	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
290	289	adantlr 712	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
291		simpl 483	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
292		elunnel1 4084	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 ∈ {𝑍})
293		elsni 4578	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
294	292, 293	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
295	294	adantll 711	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
296		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
297	296	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑐‘𝑍))
298	3	nn0cnd 12295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ ℂ)
299	298	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
300	299, 123	nncand 11337	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝑐‘𝑍))
301	300	eqcomd 2744	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
302	301	adantrr 714	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
303	302	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
304	255	fveq2d 6778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
305	258, 225	op1st 7839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍))
306	305	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍)))
307	304, 306	eqtr2d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) = (1^st ‘(𝐷‘𝑐)))
308	307	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
309	308	adantrr 714	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
310	309	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
311		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷‘𝑐) = (𝐷‘𝑒) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘(𝐷‘𝑒)))
312	311	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘(𝐷‘𝑒)))
313	273	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘(𝐷‘𝑒)) = (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
314	313	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑒)) = (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
315	279, 281	op1st 7839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍))
316	315	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍)))
317	312, 314, 316	3eqtrd 2782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑐)) = (𝐽 − (𝑒‘𝑍)))
318	317	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝐽 − (𝐽 − (𝑒‘𝑍))))
319	298	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
320		zsscn 12327	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℤ ⊆ ℂ
321	105, 320	sstri 3930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0...𝐽) ⊆ ℂ
322	321	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
323		eleq1w 2821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
324	323	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
325		feq1 6581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
326	324, 325	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
327	326, 45	chvarvv 2002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
328	50	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
329	327, 328	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ (0...𝐽))
330	322, 329	sseldd 3922	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ ℂ)
331	319, 330	nncand 11337	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
332	331	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
333		eqidd 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑒‘𝑍) = (𝑒‘𝑍))
334	318, 332, 333	3eqtrd 2782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
335	334	adantlrl 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
336	303, 310, 335	3eqtrd 2782	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝑒‘𝑍))
337	336	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑍) = (𝑒‘𝑍))
338		fveq2 6774	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑡) = (𝑒‘𝑍))
339	338	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑍) = (𝑒‘𝑡))
340	339	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑒‘𝑍) = (𝑒‘𝑡))
341	297, 337, 340	3eqtrd 2782	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
342	341	adantlr 712	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
343	291, 295, 342	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
344	290, 343	pm2.61dan 810	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐‘𝑡) = (𝑒‘𝑡))
345	344	ex 413	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → (𝑐‘𝑡) = (𝑒‘𝑡)))
346	248, 345	ralrimi 3141	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡))
347	67	adantrr 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
348	347	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
349	327	ffnd 6601	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
350	349	adantrl 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
351	350	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
352		eqfnfv 6909	. . . . . . . . 9 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
353	348, 351, 352	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
354	346, 353	mpbird 256	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 = 𝑒)
355	354	ex 413	. . . . . 6 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
356	355	ralrimivva 3123	. . . . 5 ⊢ (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
357	243, 356	jca 512	. . . 4 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
358		dff13 7128	. . . 4 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
359	357, 358	sylibr 233	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
360		eliun 4928	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
361	360	biimpi 215	. . . . . . . . . 10 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
362	361	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
363		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑘𝜑
364		nfcv 2907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝑝
365		nfiu1 4958	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
366	364, 365	nfel 2921	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
367	363, 366	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
368		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}
369		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑘 ∈ (0...𝐽)
370		nfcv 2907	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑝
371		nfcv 2907	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑘}
372		nfcv 2907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡𝑅
373	84, 372	nffv 6784	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝐶‘𝑅)
374		nfcv 2907	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝑘
375	373, 374	nffv 6784	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝐶‘𝑅)‘𝑘)
376	371, 375	nfxp 5622	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡({𝑘} × ((𝐶‘𝑅)‘𝑘))
377	370, 376	nfel 2921	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))
378	72, 369, 377	nf3an 1904	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
379		0zd 12331	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
380	4	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
381	380	3ad2antl1 1184	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
382		iftrue 4465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ 𝑅 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
383	382	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
384		simp1 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝜑)
385		simp2 1136	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
386		xp2nd 7864	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (2^nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
387	386	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
388	187	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
389		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
390	389	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ((0...𝑛) ↑_m 𝑅) = ((0...𝑘) ↑_m 𝑅))
391		rabeq 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((0...𝑛) ↑_m 𝑅) = ((0...𝑘) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
392	390, 391	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
393		eqeq2 2750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘))
394	393	rabbidv 3414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
395	392, 394	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
396	395	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
397		elfznn0 13349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ₀)
398	397	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ₀)
399		ovex 7308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0...𝑘) ↑_m 𝑅) ∈ V
400	399	rabex 5256	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V
401	400	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V)
402	388, 396, 398, 401	fvmptd 6882	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
403	402	3adant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
404	387, 403	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
405		elrabi 3618	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
406	405	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ (2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘}) → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
407	384, 385, 404, 406	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
408		elmapi 8637	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
409	407, 408	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
410	409	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
411	410	ffvelrnda 6961	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
412	411	elfzelzd 13257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
413	383, 412	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
414		simpl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
415	294	adantll 711	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
416		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
417	128	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
418	416, 417	eqneltrd 2858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
419	418	iffalsed 4470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
420	419	3ad2antl1 1184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
421	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
422	421	3ad2antl1 1184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
423		xp1st 7863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ {𝑘})
424		elsni 4578	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1^st ‘𝑝) ∈ {𝑘} → (1^st ‘𝑝) = 𝑘)
425	423, 424	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) = 𝑘)
426	425	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) = 𝑘)
427	105	sseli 3917	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
428	427	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
429	426, 428	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ ℤ)
430	429	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ ℤ)
431	430	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1^st ‘𝑝) ∈ ℤ)
432	422, 431	zsubcld 12431	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1^st ‘𝑝)) ∈ ℤ)
433	420, 432	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
434	433	adantlr 712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
435	414, 415, 434	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
436	413, 435	pm2.61dan 810	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
437	409	ffvelrnda 6961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
438		elfzle1 13259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2^nd ‘𝑝)‘𝑡))
439	437, 438	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ ((2^nd ‘𝑝)‘𝑡))
440	382	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ 𝑅 → ((2^nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
441	440	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
442	439, 441	breqtrd 5100	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
443	442	adantlr 712	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
444		simpll 764	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))))
445		elfzle2 13260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ≤ 𝐽)
446		elfzel2 13254	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
447	446	zred 12426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
448	107	sseli 3917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
449	447, 448	subge0d 11565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽 − 𝑘) ↔ 𝑘 ≤ 𝐽))
450	445, 449	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽 − 𝑘))
451	450	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
452	451	3ad2antl2 1185	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
453	384, 418	sylan 580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
454	453	iffalsed 4470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
455	426	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) = 𝑘)
456	455	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) = (𝐽 − 𝑘))
457	456	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1^st ‘𝑝)) = (𝐽 − 𝑘))
458	454, 457	eqtr2d 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
459	452, 458	breqtrd 5100	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
460	444, 415, 459	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
461	443, 460	pm2.61dan 810	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
462		simpl2 1191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 𝑘 ∈ (0...𝐽))
463		fzssz 13258	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0...𝑘) ⊆ ℤ
464	463	sseli 3917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
465	464	zred 12426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ∈ ℝ)
466	465	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ∈ ℝ)
467	448	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
468	447	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
469		elfzle2 13260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝑘)
470	469	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝑘)
471	445	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ≤ 𝐽)
472	466, 467, 468, 470, 471	letrd 11132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
473	437, 462, 472	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
474	473	adantlr 712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
475	383, 474	eqbrtrd 5096	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
476	458	eqcomd 2744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − 𝑘))
477	398	nn0ge0d 12296	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
478	447	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
479	448	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
480	478, 479	subge02d 11567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽 − 𝑘) ≤ 𝐽))
481	477, 480	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐽 − 𝑘) ≤ 𝐽)
482	481	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
483	482	3adantl3 1167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
484	476, 483	eqbrtrd 5096	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
485	444, 415, 484	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
486	475, 485	pm2.61dan 810	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
487	379, 381, 436, 461, 486	elfzd 13247	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ (0...𝐽))
488		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
489	378, 487, 488	fmptdf 6991	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
490		ovexd 7310	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (0...𝐽) ∈ V)
491	384, 18	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
492	490, 491	elmapd 8629	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ↔ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽)))
493	489, 492	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
494		eqidd 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
495		eleq1w 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑡 → (𝑟 ∈ 𝑅 ↔ 𝑡 ∈ 𝑅))
496		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑡 → ((2^nd ‘𝑝)‘𝑟) = ((2^nd ‘𝑝)‘𝑡))
497	495, 496	ifbieq1d 4483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑡 → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
498	497	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑟 = 𝑡) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
499		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
500	494, 498, 499, 436	fvmptd 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
501	500	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
502	378, 501	ralrimi 3141	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
503	502	sumeq2d 15414	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
504		nfcv 2907	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))
505	384, 103	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑅 ∈ Fin)
506	384, 46	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑍 ∈ 𝑇)
507	384, 128	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ¬ 𝑍 ∈ 𝑅)
508	382	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
509	437	elfzelzd 13257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
510	509	zcnd 12427	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℂ)
511	508, 510	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℂ)
512		eleq1 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑍 → (𝑡 ∈ 𝑅 ↔ 𝑍 ∈ 𝑅))
513		fveq2 6774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑍 → ((2^nd ‘𝑝)‘𝑡) = ((2^nd ‘𝑝)‘𝑍))
514	512, 513	ifbieq1d 4483	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))))
515	128	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ¬ 𝑍 ∈ 𝑅)
516	515	iffalsed 4470	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
517	516	3adant2 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
518	4	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
519	518, 430	zsubcld 12431	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) ∈ ℤ)
520	519	zcnd 12427	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) ∈ ℂ)
521	517, 520	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) ∈ ℂ)
522	378, 504, 505, 506, 507, 511, 514, 521	fsumsplitsn 15456	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))))
523	382	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡)))
524	378, 523	ralrimi 3141	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
525	524	sumeq2d 15414	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡))
526		eqidd 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (2^nd ‘𝑝) → 𝑅 = 𝑅)
527		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐 = (2^nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → 𝑐 = (2^nd ‘𝑝))
528	527	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 = (2^nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((2^nd ‘𝑝)‘𝑡))
529	526, 528	sumeq12rdv 15419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = (2^nd ‘𝑝) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡))
530	529	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (2^nd ‘𝑝) → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘 ↔ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
531	530	elrab 3624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ↔ ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
532	404, 531	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
533	532	simprd 496	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘)
534	525, 533	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = 𝑘)
535	507	iffalsed 4470	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
536	535, 456	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − 𝑘))
537	534, 536	oveq12d 7293	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))) = (𝑘 + (𝐽 − 𝑘)))
538	321	sseli 3917	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
539	538	3ad2ant2 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
540	384, 298	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
541	539, 540	pncan3d 11335	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 + (𝐽 − 𝑘)) = 𝐽)
542	537, 541	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))) = 𝐽)
543	503, 522, 542	3eqtrd 2782	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽)
544	493, 543	jca 512	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
545		eleq1w 2821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑟 → (𝑡 ∈ 𝑅 ↔ 𝑟 ∈ 𝑅))
546		fveq2 6774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑟 → ((2^nd ‘𝑝)‘𝑡) = ((2^nd ‘𝑝)‘𝑟))
547	545, 546	ifbieq1d 4483	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑟 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))
548	547	cbvmptv 5187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))
549	548	eqeq2i 2751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
550	549	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
551		fveq1 6773	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) → (𝑐‘𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡))
552	551	sumeq2sdv 15416	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡))
553	550, 552	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡))
554	553	eqeq1d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
555	554	elrab 3624	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ↔ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
556	544, 555	sylibr 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
557	556	3exp 1118	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
558	557	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
559	367, 368, 558	rexlimd 3250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}))
560	362, 559	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
561	37	eqcomd 2744	. . . . . . . . 9 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
562	561	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
563	560, 562	eleqtrd 2841	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
564	242	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
565		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
566	548	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
567	565, 566	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
568		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → 𝑟 = 𝑍)
569	128	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
570	568, 569	eqneltrd 2858	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑟 ∈ 𝑅)
571	570	iffalsed 4470	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
572	571	adantlr 712	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
573	50	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
574		ovexd 7310	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (1^st ‘𝑝)) ∈ V)
575	567, 572, 573, 574	fvmptd 6882	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐‘𝑍) = (𝐽 − (1^st ‘𝑝)))
576	575	oveq2d 7291	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1^st ‘𝑝))))
577	576	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1^st ‘𝑝))))
578	298	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝐽 ∈ ℂ)
579		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(1^st ‘𝑝) ∈ (0...𝐽)
580		simpl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
581		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → (1^st ‘𝑝) = 𝑘)
582		simpl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → 𝑘 ∈ (0...𝐽))
583	581, 582	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → (1^st ‘𝑝) ∈ (0...𝐽))
584	580, 426, 583	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ (0...𝐽))
585	584	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽)))
586	585	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽))))
587	366, 579, 586	rexlimd 3250	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽)))
588	361, 587	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽))
589	588	elfzelzd 13257	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ ℤ)
590	589	zcnd 12427	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ ℂ)
591	590	ad2antlr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (1^st ‘𝑝) ∈ ℂ)
592	578, 591	nncand 11337	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝐽 − (1^st ‘𝑝))) = (1^st ‘𝑝))
593	577, 592	eqtrd 2778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (1^st ‘𝑝))
594		reseq1 5885	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (𝑐 ↾ 𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅))
595	594	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐 ↾ 𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅))
596	68	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
597	596	resmptd 5948	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅) = (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
598		nfv 1917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝)
599	382	mpteq2ia 5177	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡))
600	599	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡)))
601	409	feqmptd 6837	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡)))
602	600, 601	eqtr4d 2781	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
603	602	3exp 1118	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))))
604	603	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))))
605	367, 598, 604	rexlimd 3250	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝)))
606	362, 605	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
607	606	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
608	595, 597, 607	3eqtrd 2782	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐 ↾ 𝑅) = (2^nd ‘𝑝))
609	593, 608	opeq12d 4812	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
610		opex 5379	. . . . . . . . . 10 ⊢ ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ ∈ V
611	610	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ ∈ V)
612	564, 609, 563, 611	fvmptd 6882	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
613		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑘⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝
614		1st2nd2 7870	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → 𝑝 = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
615	614	eqcomd 2744	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝)
616	615	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝))
617	616	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝)))
618	367, 613, 617	rexlimd 3250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝))
619	362, 618	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝)
620	612, 619	eqtr2d 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))))
621		fveq2 6774	. . . . . . . 8 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (𝐷‘𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))))
622	621	rspceeqv 3575	. . . . . . 7 ⊢ (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
623	563, 620, 622	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
624	623	ralrimiva 3103	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
625	243, 624	jca 512	. . . 4 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
626		dffo3 6978	. . . 4 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
627	625, 626	sylibr 233	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
628	359, 627	jca 512	. 2 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))))
629		df-f1o 6440	. 2 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))))
630	628, 629	sylibr 233	1 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 {crab 3068 Vcvv 3432 ∪ cun 3885 ⊆ wss 3887 ifcif 4459 𝒫 cpw 4533 {csn 4561 ⟨cop 4567 ∪ ciun 4924 class class class wbr 5074 ↦ cmpt 5157 × cxp 5587 ↾ cres 5591 Fn wfn 6428 ⟶wf 6429 –1-1→wf1 6430 –onto→wfo 6431 –1-1-onto→wf1o 6432 ‘cfv 6433 (class class class)co 7275 1^st c1st 7829 2^nd c2nd 7830 ↑_m cmap 8615 Fincfn 8733 ℂcc 10869 ℝcr 10870 0cc0 10871 + caddc 10874 ≤ cle 11010 − cmin 11205 ℕ₀cn0 12233 ℤcz 12319 ...cfz 13239 Σcsu 15397

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-map 8617 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-oi 9269 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-ico 13085 df-fz 13240 df-fzo 13383 df-seq 13722 df-exp 13783 df-hash 14045 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-clim 15197 df-sum 15398

This theorem is referenced by: dvnprodlem2 43488

W3C validator