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 45477

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 2726	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
2		0zd 12608	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3		dvnprodlem1.j	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
4	3	nn0zd 12622	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℤ)
5	4	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6		dvnprodlem1.c	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
7		oveq2 7427	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})))
8		rabeq 3433	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
9	7, 8	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
10		sumeq1 15679	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
11	10	eqeq1d 2727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛))
12	11	rabbidv 3426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
13	9, 12	eqtrd 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
14	13	mpteq2dv 5251	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
15		dvnprodlem1.rzt	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
16		dvnprodlem1.t	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ Fin)
17		ssexg 5324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∪ {𝑍}) ⊆ 𝑇 ∧ 𝑇 ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ V)
18	15, 16, 17	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
19		elpwg 4607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
21	15, 20	mpbird 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
22		nn0ex 12516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ₀ ∈ V
23	22	mptex 7235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V
24	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V)
25	6, 14, 21, 24	fvmptd3 7027	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
26		oveq2 7427	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
27	26	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝐽 → ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
28		rabeq 3433	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
30		eqeq2 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
31	30	rabbidv 3426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
32	29, 31	eqtrd 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
33	32	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
34		ovex 7452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∈ V
35	34	rabex 5335	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V
36	35	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V)
37	25, 33, 3, 36	fvmptd 7011	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
38		ssrab2 4073	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍}))
39	38	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
40	37, 39	eqsstrd 4015	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
41	40	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
42		simpr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
43	41, 42	sseldd 3977	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
44		elmapi 8868	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
45	43, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
46		dvnprodlem1.z	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ 𝑇)
47		snidg 4664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑍 ∈ 𝑇 → 𝑍 ∈ {𝑍})
48	46, 47	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
49		elun2 4175	. . . . . . . . . . . . . . . 16 ⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
50	48, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑍 ∈ (𝑅 ∪ {𝑍}))
51	50	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
52	45, 51	ffvelcdmd 7094	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ (0...𝐽))
53	52	elfzelzd 13542	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℤ)
54	5, 53	zsubcld 12709	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
55		elfzle2 13545	. . . . . . . . . . . . 13 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → (𝑐‘𝑍) ≤ 𝐽)
56	52, 55	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ≤ 𝐽)
57	5	zred 12704	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
58	53	zred 12704	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℝ)
59	57, 58	subge0d 11841	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐‘𝑍)) ↔ (𝑐‘𝑍) ≤ 𝐽))
60	56, 59	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐‘𝑍)))
61		elfzle1 13544	. . . . . . . . . . . . 13 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑍))
62	52, 61	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐‘𝑍))
63	57, 58	subge02d 11843	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐‘𝑍) ↔ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽))
64	62, 63	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)
65	2, 5, 54, 60, 64	elfzd 13532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽))
66		elmapfn 8884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
67	43, 66	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
68		ssun1 4170	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 ⊆ (𝑅 ∪ {𝑍})
69	68	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
70		fnssres 6679	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑅 ⊆ (𝑅 ∪ {𝑍})) → (𝑐 ↾ 𝑅) Fn 𝑅)
71	67, 69, 70	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) Fn 𝑅)
72		nfv 1909	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝜑
73		nfcv 2891	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡𝑐
74		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡𝒫 𝑇
75		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡ℕ₀
76		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡𝑠
77	76	nfsum1 15680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡)
78		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡𝑛
79	77, 78	nfeq 2905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛
80		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡((0...𝑛) ↑_m 𝑠)
81	79, 80	nfrabw 3456	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡{𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}
82	75, 81	nfmpt 5256	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
83	74, 82	nfmpt 5256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
84	6, 83	nfcxfr 2889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡𝐶
85		nfcv 2891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡(𝑅 ∪ {𝑍})
86	84, 85	nffv 6906	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝐶‘(𝑅 ∪ {𝑍}))
87		nfcv 2891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐽
88	86, 87	nffv 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
89	73, 88	nfel 2906	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
90	72, 89	nfan 1894	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
91		fvres 6915	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
92	91	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
93	2	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ∈ ℤ)
94	54	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
95	45	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
96	69	sselda 3976	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
97	95, 96	ffvelcdmd 7094	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...𝐽))
98	97	elfzelzd 13542	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ ℤ)
99		elfzle1 13544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐‘𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑡))
100	97, 99	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ≤ (𝑐‘𝑡))
101	15	unssad 4185	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ⊆ 𝑇)
102		ssfi 9201	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 ∈ Fin ∧ 𝑅 ⊆ 𝑇) → 𝑅 ∈ Fin)
103	16, 101, 102	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑅 ∈ Fin)
104	103	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑅 ∈ Fin)
105		fzssz 13543	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0...𝐽) ⊆ ℤ
106		zssre 12603	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ℤ ⊆ ℝ
107	105, 106	sstri 3986	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0...𝐽) ⊆ ℝ
108	107	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (0...𝐽) ⊆ ℝ)
109	45	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
110	69	sselda 3976	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
111	109, 110	ffvelcdmd 7094	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ (0...𝐽))
112	108, 111	sseldd 3977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
113	112	adantlr 713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
114		elfzle1 13544	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐‘𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑟))
115	111, 114	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
116	115	adantlr 713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
117		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟 = 𝑡 → (𝑐‘𝑟) = (𝑐‘𝑡))
118		simpr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ 𝑅)
119	104, 113, 116, 117, 118	fsumge1 15787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
120	103	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
121	112	recnd 11279	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℂ)
122	120, 121	fsumcl 15723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) ∈ ℂ)
123	58	recnd 11279	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℂ)
124	122, 123	pncand 11609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) − (𝑐‘𝑍)) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
125		nfv 1909	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑟(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
126		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑟(𝑐‘𝑍)
127	46	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ 𝑇)
128		dvnprodlem1.zr	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑅)
129	128	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍 ∈ 𝑅)
130		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑟 = 𝑍 → (𝑐‘𝑟) = (𝑐‘𝑍))
131	125, 126, 120, 127, 129, 121, 130, 123	fsumsplitsn 15734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)))
132	131	eqcomd 2731	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟))
133	117	cbvsumv 15686	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡)
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
135	37	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
136	42, 135	eleqtrd 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
137		rabid 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
138	136, 137	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
139	138	simprd 494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽)
140	134, 139	eqtrd 2765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = 𝐽)
141	132, 140	eqtrd 2765	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = 𝐽)
142	141	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) − (𝑐‘𝑍)) = (𝐽 − (𝑐‘𝑍)))
143	124, 142	eqtr3d 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
144	143	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
145	119, 144	breqtrd 5175	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))
146	93, 94, 98, 100, 145	elfzd 13532	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
147	92, 146	eqeltrd 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
148	147	ex 411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
149	90, 148	ralrimi 3244	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
150	71, 149	jca 510	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
151		ffnfv 7128	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))) ↔ ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
152	150, 151	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))))
153		ovexd 7454	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐‘𝑍))) ∈ V)
154	16, 101	ssexd 5325	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ V)
155	154	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ V)
156	153, 155	elmapd 8859	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ↔ (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍)))))
157	152, 156	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅))
158	91	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡)))
159	90, 158	ralrimi 3244	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
160	159	sumeq2d 15692	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
161	117	cbvsumv 15686	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡)
162	161	eqcomi 2734	. . . . . . . . . . . . . . 15 ⊢ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟)
163	162	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
164	143	idi 1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
165	160, 163, 164	3eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍)))
166	157, 165	jca 510	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
167		eqidd 2726	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → 𝑅 = 𝑅)
168		simpl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → 𝑒 = (𝑐 ↾ 𝑅))
169	168	fveq1d 6898	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → (𝑒‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
170	167, 169	sumeq12rdv 15697	. . . . . . . . . . . . . 14 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡))
171	170	eqeq1d 2727	. . . . . . . . . . . . 13 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍)) ↔ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
172	171	elrab 3679	. . . . . . . . . . . 12 ⊢ ((𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ↔ ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
173	166, 172	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
174		oveq2 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑅 → ((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m 𝑅))
175		rabeq 3433	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
176	174, 175	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
177		sumeq1 15679	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑅 → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
178	177	eqeq1d 2727	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑅 → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛))
179	178	rabbidv 3426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
180	176, 179	eqtrd 2765	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
181	180	mpteq2dv 5251	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑅 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
182		elpwg 4607	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇 ↔ 𝑅 ⊆ 𝑇))
183	154, 182	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ∈ 𝒫 𝑇 ↔ 𝑅 ⊆ 𝑇))
184	101, 183	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ 𝒫 𝑇)
185	22	mptex 7235	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V
186	185	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V)
187	6, 181, 184, 186	fvmptd3 7027	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
188	187	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
189		oveq2 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
190	189	oveq1d 7434	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((0...𝑛) ↑_m 𝑅) = ((0...𝑚) ↑_m 𝑅))
191		rabeq 3433	. . . . . . . . . . . . . . . . . 18 ⊢ (((0...𝑛) ↑_m 𝑅) = ((0...𝑚) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
192	190, 191	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
193		eqeq2 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚))
194	193	rabbidv 3426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
195	192, 194	eqtrd 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
196	195	cbvmptv 5262	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
197	196	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
198	188, 197	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
199		fveq1 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑡) = (𝑒‘𝑡))
200	199	sumeq2sdv 15694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑒 → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑒‘𝑡))
201	200	eqeq1d 2727	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚))
202	201	cbvrabv 3429	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚}
203	202	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
204		oveq2 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐‘𝑍))))
205	204	oveq1d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → ((0...𝑚) ↑_m 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅))
206		rabeq 3433	. . . . . . . . . . . . . . . 16 ⊢ (((0...𝑚) ↑_m 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) → {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
207	205, 206	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
208		eqeq2 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))))
209	208	rabbidv 3426	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
210	203, 207, 209	3eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
211	210	adantl 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑚 = (𝐽 − (𝑐‘𝑍))) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
212	54, 60	jca 510	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
213		elnn0z 12609	. . . . . . . . . . . . . 14 ⊢ ((𝐽 − (𝑐‘𝑍)) ∈ ℕ₀ ↔ ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
214	212, 213	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℕ₀)
215		ovex 7452	. . . . . . . . . . . . . . 15 ⊢ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∈ V
216	215	rabex 5335	. . . . . . . . . . . . . 14 ⊢ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V
217	216	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V)
218	198, 211, 214, 217	fvmptd 7011	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
219	218	eqcomd 2731	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
220	173, 219	eleqtrd 2827	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
221	65, 220	jca 510	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
222	1, 221	jca 510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
223		ovexd 7454	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ V)
224		vex 3465	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
225	224	resex 6034	. . . . . . . . . 10 ⊢ (𝑐 ↾ 𝑅) ∈ V
226	225	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ V)
227		opeq12 4877	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
228	227	eqeq2d 2736	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
229		eleq1 2813	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
230	229	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
231		simpr 483	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → 𝑑 = (𝑐 ↾ 𝑅))
232		fveq2 6896	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
233	232	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
234	231, 233	eleq12d 2819	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑑 ∈ ((𝐶‘𝑅)‘𝑘) ↔ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
235	230, 234	anbi12d 630	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
236	228, 235	anbi12d 630	. . . . . . . . . 10 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))))
237	236	spc2egv 3583	. . . . . . . . 9 ⊢ (((𝐽 − (𝑐‘𝑍)) ∈ V ∧ (𝑐 ↾ 𝑅) ∈ V) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
238	223, 226, 237	syl2anc 582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
239	222, 238	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
240		eliunxp 5840	. . . . . . 7 ⊢ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
241	239, 240	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
242		dvnprodlem1.d	. . . . . 6 ⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
243	241, 242	fmptd 7123	. . . . 5 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
244	88	nfcri 2882	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
245	89, 244	nfan 1894	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
246	72, 245	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
247		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝐷‘𝑐) = (𝐷‘𝑒)
248	246, 247	nfan 1894	. . . . . . . . 9 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒))
249	92	eqcomd 2731	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
250	249	adantlrr 719	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
251	250	adantlr 713	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
252	242	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
253		opex 5466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V
254	253	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V)
255	252, 254	fvmpt2d 7017	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
256	255	fveq2d 6900	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
257	256	fveq1d 6898	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡))
258		ovex 7452	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 − (𝑐‘𝑍)) ∈ V
259	258, 225	op2nd 8003	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝑐 ↾ 𝑅)
260	259	fveq1i 6897	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡)
261	260	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
262	257, 261	eqtr2d 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
263	262	adantrr 715	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
264	263	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
265		simpr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = (𝐷‘𝑒))
266		fveq1 6895	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑍) = (𝑒‘𝑍))
267	266	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝑒‘𝑍)))
268		reseq1 5979	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (𝑐 ↾ 𝑅) = (𝑒 ↾ 𝑅))
269	267, 268	opeq12d 4883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
270		simpr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
271		opex 5466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V
272	271	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V)
273	242, 269, 270, 272	fvmptd3 7027	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
274	273	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
275	265, 274	eqtrd 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
276	275	fveq2d 6900	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
277	276	adantlrl 718	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
278	277	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
279		ovex 7452	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 − (𝑒‘𝑍)) ∈ V
280		vex 3465	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑒 ∈ V
281	280	resex 6034	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ↾ 𝑅) ∈ V
282	279, 281	op2nd 8003	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅)
283	282	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅))
284	278, 283	eqtrd 2765	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘(𝐷‘𝑐)) = (𝑒 ↾ 𝑅))
285	284	fveq1d 6898	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = ((𝑒 ↾ 𝑅)‘𝑡))
286		fvres 6915	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝑅 → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
287	286	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
288	285, 287	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = (𝑒‘𝑡))
289	251, 264, 288	3eqtrd 2769	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
290	289	adantlr 713	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
291		simpl 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
292		elunnel1 4146	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 ∈ {𝑍})
293		elsni 4647	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
294	292, 293	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
295	294	adantll 712	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
296		simpr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
297	296	fveq2d 6900	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑐‘𝑍))
298	3	nn0cnd 12572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ ℂ)
299	298	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
300	299, 123	nncand 11613	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝑐‘𝑍))
301	300	eqcomd 2731	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
302	301	adantrr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
303	302	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
304	255	fveq2d 6900	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
305	258, 225	op1st 8002	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍))
306	305	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍)))
307	304, 306	eqtr2d 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) = (1^st ‘(𝐷‘𝑐)))
308	307	oveq2d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
309	308	adantrr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
310	309	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
311		fveq2 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷‘𝑐) = (𝐷‘𝑒) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘(𝐷‘𝑒)))
312	311	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘(𝐷‘𝑒)))
313	273	fveq2d 6900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘(𝐷‘𝑒)) = (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
314	313	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑒)) = (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
315	279, 281	op1st 8002	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍))
316	315	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍)))
317	312, 314, 316	3eqtrd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑐)) = (𝐽 − (𝑒‘𝑍)))
318	317	oveq2d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝐽 − (𝐽 − (𝑒‘𝑍))))
319	298	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
320		zsscn 12604	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℤ ⊆ ℂ
321	105, 320	sstri 3986	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0...𝐽) ⊆ ℂ
322	321	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
323		eleq1w 2808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
324	323	anbi2d 628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
325		feq1 6704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
326	324, 325	imbi12d 343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
327	326, 45	chvarvv 1994	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
328	50	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
329	327, 328	ffvelcdmd 7094	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ (0...𝐽))
330	322, 329	sseldd 3977	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ ℂ)
331	319, 330	nncand 11613	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
332	331	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
333		eqidd 2726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑒‘𝑍) = (𝑒‘𝑍))
334	318, 332, 333	3eqtrd 2769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
335	334	adantlrl 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
336	303, 310, 335	3eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝑒‘𝑍))
337	336	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑍) = (𝑒‘𝑍))
338		fveq2 6896	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑡) = (𝑒‘𝑍))
339	338	eqcomd 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑍) = (𝑒‘𝑡))
340	339	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑒‘𝑍) = (𝑒‘𝑡))
341	297, 337, 340	3eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
342	341	adantlr 713	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
343	291, 295, 342	syl2anc 582	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
344	290, 343	pm2.61dan 811	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐‘𝑡) = (𝑒‘𝑡))
345	344	ex 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → (𝑐‘𝑡) = (𝑒‘𝑡)))
346	248, 345	ralrimi 3244	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡))
347	67	adantrr 715	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
348	347	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
349	327	ffnd 6724	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
350	349	adantrl 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
351	350	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
352		eqfnfv 7039	. . . . . . . . 9 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
353	348, 351, 352	syl2anc 582	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
354	346, 353	mpbird 256	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 = 𝑒)
355	354	ex 411	. . . . . 6 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
356	355	ralrimivva 3190	. . . . 5 ⊢ (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
357	243, 356	jca 510	. . . 4 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
358		dff13 7265	. . . 4 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
359	357, 358	sylibr 233	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
360		eliun 5001	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
361	360	biimpi 215	. . . . . . . . . 10 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
362	361	adantl 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
363		nfv 1909	. . . . . . . . . . 11 ⊢ Ⅎ𝑘𝜑
364		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝑝
365		nfiu1 5031	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
366	364, 365	nfel 2906	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
367	363, 366	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
368		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}
369		nfv 1909	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑘 ∈ (0...𝐽)
370		nfcv 2891	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑝
371		nfcv 2891	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑘}
372		nfcv 2891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡𝑅
373	84, 372	nffv 6906	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝐶‘𝑅)
374		nfcv 2891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝑘
375	373, 374	nffv 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝐶‘𝑅)‘𝑘)
376	371, 375	nfxp 5711	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡({𝑘} × ((𝐶‘𝑅)‘𝑘))
377	370, 376	nfel 2906	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))
378	72, 369, 377	nf3an 1896	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
379		0zd 12608	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
380	4	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
381	380	3ad2antl1 1182	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
382		iftrue 4536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ 𝑅 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
383	382	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
384		simp1 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝜑)
385		simp2 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
386		xp2nd 8027	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (2^nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
387	386	3ad2ant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
388	187	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
389		oveq2 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
390	389	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ((0...𝑛) ↑_m 𝑅) = ((0...𝑘) ↑_m 𝑅))
391		rabeq 3433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((0...𝑛) ↑_m 𝑅) = ((0...𝑘) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
392	390, 391	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
393		eqeq2 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘))
394	393	rabbidv 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
395	392, 394	eqtrd 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
396	395	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
397		elfznn0 13634	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ₀)
398	397	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ₀)
399		ovex 7452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((0...𝑘) ↑_m 𝑅) ∈ V
400	399	rabex 5335	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V
401	400	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V)
402	388, 396, 398, 401	fvmptd 7011	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
403	402	3adant3 1129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
404	387, 403	eleqtrd 2827	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
405		elrabi 3673	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
406	405	3ad2ant3 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ (2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘}) → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
407	384, 385, 404, 406	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
408		elmapi 8868	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
409	407, 408	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
410	409	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
411	410	ffvelcdmda 7093	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
412	411	elfzelzd 13542	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
413	383, 412	eqeltrd 2825	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
414		simpl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
415	294	adantll 712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
416		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
417	128	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
418	416, 417	eqneltrd 2845	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
419	418	iffalsed 4541	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
420	419	3ad2antl1 1182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
421	4	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
422	421	3ad2antl1 1182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
423		xp1st 8026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ {𝑘})
424		elsni 4647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1^st ‘𝑝) ∈ {𝑘} → (1^st ‘𝑝) = 𝑘)
425	423, 424	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) = 𝑘)
426	425	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) = 𝑘)
427	105	sseli 3972	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
428	427	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
429	426, 428	eqeltrd 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ ℤ)
430	429	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ ℤ)
431	430	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1^st ‘𝑝) ∈ ℤ)
432	422, 431	zsubcld 12709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1^st ‘𝑝)) ∈ ℤ)
433	420, 432	eqeltrd 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
434	433	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
435	414, 415, 434	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
436	413, 435	pm2.61dan 811	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
437	409	ffvelcdmda 7093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
438		elfzle1 13544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2^nd ‘𝑝)‘𝑡))
439	437, 438	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ ((2^nd ‘𝑝)‘𝑡))
440	382	eqcomd 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ 𝑅 → ((2^nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
441	440	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
442	439, 441	breqtrd 5175	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
443	442	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
444		simpll 765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))))
445		elfzle2 13545	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ≤ 𝐽)
446		elfzel2 13539	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
447	446	zred 12704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
448	107	sseli 3972	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
449	447, 448	subge0d 11841	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽 − 𝑘) ↔ 𝑘 ≤ 𝐽))
450	445, 449	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽 − 𝑘))
451	450	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
452	451	3ad2antl2 1183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
453	384, 418	sylan 578	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
454	453	iffalsed 4541	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
455	426	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) = 𝑘)
456	455	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) = (𝐽 − 𝑘))
457	456	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1^st ‘𝑝)) = (𝐽 − 𝑘))
458	454, 457	eqtr2d 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
459	452, 458	breqtrd 5175	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
460	444, 415, 459	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
461	443, 460	pm2.61dan 811	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
462		simpl2 1189	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 𝑘 ∈ (0...𝐽))
463		fzssz 13543	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0...𝑘) ⊆ ℤ
464	463	sseli 3972	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
465	464	zred 12704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ∈ ℝ)
466	465	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ∈ ℝ)
467	448	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
468	447	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
469		elfzle2 13545	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝑘)
470	469	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝑘)
471	445	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ≤ 𝐽)
472	466, 467, 468, 470, 471	letrd 11408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
473	437, 462, 472	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
474	473	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
475	383, 474	eqbrtrd 5171	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
476	458	eqcomd 2731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − 𝑘))
477	398	nn0ge0d 12573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
478	447	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
479	448	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
480	478, 479	subge02d 11843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽 − 𝑘) ≤ 𝐽))
481	477, 480	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐽 − 𝑘) ≤ 𝐽)
482	481	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
483	482	3adantl3 1165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
484	476, 483	eqbrtrd 5171	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
485	444, 415, 484	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
486	475, 485	pm2.61dan 811	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
487	379, 381, 436, 461, 486	elfzd 13532	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ (0...𝐽))
488		eqid 2725	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
489	378, 487, 488	fmptdf 7126	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
490		ovexd 7454	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (0...𝐽) ∈ V)
491	384, 18	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
492	490, 491	elmapd 8859	. . . . . . . . . . . . . . 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 2726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
495		eleq1w 2808	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑡 → (𝑟 ∈ 𝑅 ↔ 𝑡 ∈ 𝑅))
496		fveq2 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑡 → ((2^nd ‘𝑝)‘𝑟) = ((2^nd ‘𝑝)‘𝑡))
497	495, 496	ifbieq1d 4554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑡 → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
498	497	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑟 = 𝑡) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
499		simpr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
500	494, 498, 499, 436	fvmptd 7011	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
501	500	ex 411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
502	378, 501	ralrimi 3244	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
503	502	sumeq2d 15692	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
504		nfcv 2891	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
509	437	elfzelzd 13542	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
510	509	zcnd 12705	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℂ)
511	508, 510	eqeltrd 2825	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℂ)
512		eleq1 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑍 → (𝑡 ∈ 𝑅 ↔ 𝑍 ∈ 𝑅))
513		fveq2 6896	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑍 → ((2^nd ‘𝑝)‘𝑡) = ((2^nd ‘𝑝)‘𝑍))
514	512, 513	ifbieq1d 4554	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))))
515	128	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ¬ 𝑍 ∈ 𝑅)
516	515	iffalsed 4541	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
517	516	3adant2 1128	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
518	4	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
519	518, 430	zsubcld 12709	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) ∈ ℤ)
520	519	zcnd 12705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) ∈ ℂ)
521	517, 520	eqeltrd 2825	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) ∈ ℂ)
522	378, 504, 505, 506, 507, 511, 514, 521	fsumsplitsn 15734	. . . . . . . . . . . . . . 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 3244	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
525	524	sumeq2d 15692	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡))
526		eqidd 2726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (2^nd ‘𝑝) → 𝑅 = 𝑅)
527		simpl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐 = (2^nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → 𝑐 = (2^nd ‘𝑝))
528	527	fveq1d 6898	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 = (2^nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((2^nd ‘𝑝)‘𝑡))
529	526, 528	sumeq12rdv 15697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = (2^nd ‘𝑝) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡))
530	529	eqeq1d 2727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (2^nd ‘𝑝) → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘 ↔ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
531	530	elrab 3679	. . . . . . . . . . . . . . . . . . . 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 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘)
534	525, 533	eqtrd 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = 𝑘)
535	507	iffalsed 4541	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
536	535, 456	eqtrd 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − 𝑘))
537	534, 536	oveq12d 7437	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))) = (𝑘 + (𝐽 − 𝑘)))
538	321	sseli 3972	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
539	538	3ad2ant2 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
540	384, 298	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
541	539, 540	pncan3d 11611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 + (𝐽 − 𝑘)) = 𝐽)
542	537, 541	eqtrd 2765	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))) = 𝐽)
543	503, 522, 542	3eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽)
544	493, 543	jca 510	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
545		eleq1w 2808	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑟 → (𝑡 ∈ 𝑅 ↔ 𝑟 ∈ 𝑅))
546		fveq2 6896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑟 → ((2^nd ‘𝑝)‘𝑡) = ((2^nd ‘𝑝)‘𝑟))
547	545, 546	ifbieq1d 4554	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑟 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))
548	547	cbvmptv 5262	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))
549	548	eqeq2i 2738	. . . . . . . . . . . . . . . . 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 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) → (𝑐‘𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡))
552	551	sumeq2sdv 15694	. . . . . . . . . . . . . . . 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 2727	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
555	554	elrab 3679	. . . . . . . . . . . . 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 1116	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
558	557	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
559	367, 368, 558	rexlimd 3253	. . . . . . . . 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 2731	. . . . . . . . 9 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
562	561	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
563	560, 562	eleqtrd 2827	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
564	242	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
565		simpr 483	. . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
568		simpr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → 𝑟 = 𝑍)
569	128	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
570	568, 569	eqneltrd 2845	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑟 ∈ 𝑅)
571	570	iffalsed 4541	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
572	571	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
573	50	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
574		ovexd 7454	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (1^st ‘𝑝)) ∈ V)
575	567, 572, 573, 574	fvmptd 7011	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐‘𝑍) = (𝐽 − (1^st ‘𝑝)))
576	575	oveq2d 7435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1^st ‘𝑝))))
577	576	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1^st ‘𝑝))))
578	298	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝐽 ∈ ℂ)
579		nfv 1909	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(1^st ‘𝑝) ∈ (0...𝐽)
580		simpl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
581		simpr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → (1^st ‘𝑝) = 𝑘)
582		simpl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → 𝑘 ∈ (0...𝐽))
583	581, 582	eqeltrd 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → (1^st ‘𝑝) ∈ (0...𝐽))
584	580, 426, 583	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ (0...𝐽))
585	584	ex 411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽)))
586	585	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽))))
587	366, 579, 586	rexlimd 3253	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽)))
588	361, 587	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽))
589	588	elfzelzd 13542	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ ℤ)
590	589	zcnd 12705	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ ℂ)
591	590	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (1^st ‘𝑝) ∈ ℂ)
592	578, 591	nncand 11613	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝐽 − (1^st ‘𝑝))) = (1^st ‘𝑝))
593	577, 592	eqtrd 2765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (1^st ‘𝑝))
594		reseq1 5979	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (𝑐 ↾ 𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅))
595	594	adantl 480	. . . . . . . . . . 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 6045	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅) = (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
598		nfv 1909	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝)
599	382	mpteq2ia 5252	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡))
600	599	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡)))
601	409	feqmptd 6966	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡)))
602	600, 601	eqtr4d 2768	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
603	602	3exp 1116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))))
604	603	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))))
605	367, 598, 604	rexlimd 3253	. . . . . . . . . . . . 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 479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
608	595, 597, 607	3eqtrd 2769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐 ↾ 𝑅) = (2^nd ‘𝑝))
609	593, 608	opeq12d 4883	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
610		opex 5466	. . . . . . . . . 10 ⊢ ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ ∈ V
611	610	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ ∈ V)
612	564, 609, 563, 611	fvmptd 7011	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
613		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑘⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝
614		1st2nd2 8033	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → 𝑝 = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
615	614	eqcomd 2731	. . . . . . . . . . . 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 3253	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝))
619	362, 618	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝)
620	612, 619	eqtr2d 2766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))))
621		fveq2 6896	. . . . . . . 8 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (𝐷‘𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))))
622	621	rspceeqv 3628	. . . . . . 7 ⊢ (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
623	563, 620, 622	syl2anc 582	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
624	623	ralrimiva 3135	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
625	243, 624	jca 510	. . . 4 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
626		dffo3 7111	. . . 4 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
627	625, 626	sylibr 233	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
628	359, 627	jca 510	. 2 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))))
629		df-f1o 6556	. 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 394 ∧ w3a 1084 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ∀wral 3050 ∃wrex 3059 {crab 3418 Vcvv 3461 ∪ cun 3942 ⊆ wss 3944 ifcif 4530 𝒫 cpw 4604 {csn 4630 ⟨cop 4636 ∪ ciun 4997 class class class wbr 5149 ↦ cmpt 5232 × cxp 5676 ↾ cres 5680 Fn wfn 6544 ⟶wf 6545 –1-1→wf1 6546 –onto→wfo 6547 –1-1-onto→wf1o 6548 ‘cfv 6549 (class class class)co 7419 1^st c1st 7992 2^nd c2nd 7993 ↑_m cmap 8845 Fincfn 8964 ℂcc 11143 ℝcr 11144 0cc0 11145 + caddc 11148 ≤ cle 11286 − cmin 11481 ℕ₀cn0 12510 ℤcz 12596 ...cfz 13524 Σcsu 15676

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 ax-inf2 9671 ax-cnex 11201 ax-resscn 11202 ax-1cn 11203 ax-icn 11204 ax-addcl 11205 ax-addrcl 11206 ax-mulcl 11207 ax-mulrcl 11208 ax-mulcom 11209 ax-addass 11210 ax-mulass 11211 ax-distr 11212 ax-i2m1 11213 ax-1ne0 11214 ax-1rid 11215 ax-rnegex 11216 ax-rrecex 11217 ax-cnre 11218 ax-pre-lttri 11219 ax-pre-lttrn 11220 ax-pre-ltadd 11221 ax-pre-mulgt0 11222 ax-pre-sup 11223

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-int 4951 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-se 5634 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6307 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-isom 6558 df-riota 7375 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7872 df-1st 7994 df-2nd 7995 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-er 8725 df-map 8847 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-sup 9472 df-oi 9540 df-card 9969 df-pnf 11287 df-mnf 11288 df-xr 11289 df-ltxr 11290 df-le 11291 df-sub 11483 df-neg 11484 df-div 11909 df-nn 12251 df-2 12313 df-3 12314 df-n0 12511 df-z 12597 df-uz 12861 df-rp 13015 df-ico 13370 df-fz 13525 df-fzo 13668 df-seq 14008 df-exp 14068 df-hash 14334 df-cj 15090 df-re 15091 df-im 15092 df-sqrt 15226 df-abs 15227 df-clim 15476 df-sum 15677

This theorem is referenced by: dvnprodlem2 45478

W3C validator