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 42224

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 2822	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
2		0zd 11987	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3		dvnprodlem1.j	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
4	3	nn0zd 12079	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ ℤ)
5	4	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6		fzssz 12903	. . . . . . . . . . . . . . . 16 ⊢ (0...𝐽) ⊆ ℤ
7	6	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℤ)
8		dvnprodlem1.c	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
9		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})))
10		rabeq 3483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
11	9, 10	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
12		sumeq1 15039	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
13	12	eqeq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛))
14	13	rabbidv 3480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
15	11, 14	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
16	15	mpteq2dv 5154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
17		dvnprodlem1.rzt	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
18		dvnprodlem1.t	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑇 ∈ Fin)
19		ssexg 5219	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∪ {𝑍}) ⊆ 𝑇 ∧ 𝑇 ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ V)
20	17, 18, 19	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
21		elpwg 4544	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
23	17, 22	mpbird 259	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
24		nn0ex 11897	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ₀ ∈ V
25	24	mptex 6980	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V
26	25	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V)
27	8, 16, 23, 26	fvmptd3 6785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
28		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
29	28	oveq1d 7165	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝐽 → ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
30		rabeq 3483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
32		eqeq2 2833	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
33	32	rabbidv 3480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
34	31, 33	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
35	34	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
36		ovex 7183	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∈ V
37	36	rabex 5227	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V)
39	27, 35, 3, 38	fvmptd 6769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
40		ssrab2 4055	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍}))
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
42	39, 41	eqsstrd 4004	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
43	42	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
44		simpr 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
45	43, 44	sseldd 3967	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
46		elmapi 8422	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
47	45, 46	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
48		dvnprodlem1.z	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑍 ∈ 𝑇)
49		snidg 4592	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑍 ∈ 𝑇 → 𝑍 ∈ {𝑍})
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
51		elun2 4152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
52	50, 51	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ (𝑅 ∪ {𝑍}))
53	52	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
54	47, 53	ffvelrnd 6846	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ (0...𝐽))
55	7, 54	sseldd 3967	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℤ)
56	5, 55	zsubcld 12086	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
57	2, 5, 56	3jca 1124	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ))
58		elfzle2 12905	. . . . . . . . . . . . . 14 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → (𝑐‘𝑍) ≤ 𝐽)
59	54, 58	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ≤ 𝐽)
60	5	zred 12081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
61	55	zred 12081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℝ)
62	60, 61	subge0d 11224	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐‘𝑍)) ↔ (𝑐‘𝑍) ≤ 𝐽))
63	59, 62	mpbird 259	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐‘𝑍)))
64		elfzle1 12904	. . . . . . . . . . . . . 14 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑍))
65	54, 64	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐‘𝑍))
66	60, 61	subge02d 11226	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐‘𝑍) ↔ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽))
67	65, 66	mpbid 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)
68	57, 63, 67	jca32 518	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐‘𝑍)) ∧ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)))
69		elfz2 12893	. . . . . . . . . . 11 ⊢ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐‘𝑍)) ∧ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)))
70	68, 69	sylibr 236	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽))
71		elmapfn 8423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
72	45, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
73		ssun1 4147	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 ⊆ (𝑅 ∪ {𝑍})
74	73	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
75		fnssres 6464	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑅 ⊆ (𝑅 ∪ {𝑍})) → (𝑐 ↾ 𝑅) Fn 𝑅)
76	72, 74, 75	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) Fn 𝑅)
77		nfv 1911	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝜑
78		nfcv 2977	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡𝑐
79		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡𝒫 𝑇
80		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡ℕ₀
81		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡𝑠
82	81	nfsum1 15040	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡)
83		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡𝑛
84	82, 83	nfeq 2991	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛
85		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡((0...𝑛) ↑_m 𝑠)
86	84, 85	nfrabw 3385	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡{𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}
87	80, 86	nfmpt 5155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
88	79, 87	nfmpt 5155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
89	8, 88	nfcxfr 2975	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡𝐶
90		nfcv 2977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡(𝑅 ∪ {𝑍})
91	89, 90	nffv 6674	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝐶‘(𝑅 ∪ {𝑍}))
92		nfcv 2977	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐽
93	91, 92	nffv 6674	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
94	78, 93	nfel 2992	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
95	77, 94	nfan 1896	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
96		fvres 6683	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
97	96	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
98	2	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ∈ ℤ)
99	56	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
100	6	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (0...𝐽) ⊆ ℤ)
101	47	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
102	74	sselda 3966	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
103	101, 102	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...𝐽))
104	100, 103	sseldd 3967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ ℤ)
105	98, 99, 104	3jca 1124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (0 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ (𝑐‘𝑡) ∈ ℤ))
106		elfzle1 12904	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐‘𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑡))
107	103, 106	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ≤ (𝑐‘𝑡))
108	17	unssad 4162	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑅 ⊆ 𝑇)
109		ssfi 8732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑇 ∈ Fin ∧ 𝑅 ⊆ 𝑇) → 𝑅 ∈ Fin)
110	18, 108, 109	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ∈ Fin)
111	110	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑅 ∈ Fin)
112		zssre 11982	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℤ ⊆ ℝ
113	6, 112	sstri 3975	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0...𝐽) ⊆ ℝ
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (0...𝐽) ⊆ ℝ)
115	47	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
116	74	sselda 3966	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
117	115, 116	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ (0...𝐽))
118	114, 117	sseldd 3967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
119	118	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
120		elfzle1 12904	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑟))
121	117, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
122	121	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
123		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 = 𝑡 → (𝑐‘𝑟) = (𝑐‘𝑡))
124		simpr 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ 𝑅)
125	111, 119, 122, 123, 124	fsumge1 15146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
126	110	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
127	118	recnd 10663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℂ)
128	126, 127	fsumcl 15084	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) ∈ ℂ)
129	61	recnd 10663	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℂ)
130	128, 129	pncand 10992	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) − (𝑐‘𝑍)) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
131		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑟(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
132		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑟(𝑐‘𝑍)
133	48	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ 𝑇)
134		dvnprodlem1.zr	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑅)
135	134	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍 ∈ 𝑅)
136		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑟 = 𝑍 → (𝑐‘𝑟) = (𝑐‘𝑍))
137	131, 132, 126, 133, 135, 127, 136, 129	fsumsplitsn 15094	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)))
138	137	eqcomd 2827	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟))
139	123	cbvsumv 15047	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡)
140	139	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
141	39	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
142	44, 141	eleqtrd 2915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
143		rabid 3378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
144	142, 143	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
145	144	simprd 498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽)
146	140, 145	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = 𝐽)
147	138, 146	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = 𝐽)
148	147	oveq1d 7165	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) − (𝑐‘𝑍)) = (𝐽 − (𝑐‘𝑍)))
149	130, 148	eqtr3d 2858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
150	149	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
151	125, 150	breqtrd 5084	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))
152	105, 107, 151	jca32 518	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((0 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ (𝑐‘𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐‘𝑡) ∧ (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))))
153		elfz2 12893	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))) ↔ ((0 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ (𝑐‘𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐‘𝑡) ∧ (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))))
154	152, 153	sylibr 236	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
155	97, 154	eqeltrd 2913	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
156	155	ex 415	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
157	95, 156	ralrimi 3216	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
158	76, 157	jca 514	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
159		ffnfv 6876	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))) ↔ ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
160	158, 159	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))))
161		ovexd 7185	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐‘𝑍))) ∈ V)
162	18, 108	ssexd 5220	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ V)
163	162	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ V)
164	161, 163	elmapd 8414	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ↔ (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍)))))
165	160, 164	mpbird 259	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅))
166	96	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡)))
167	95, 166	ralrimi 3216	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
168	167	sumeq2d 15053	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
169	123	cbvsumv 15047	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡)
170	169	eqcomi 2830	. . . . . . . . . . . . . . 15 ⊢ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟)
171	170	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
172	149	idi 1	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
173	168, 171, 172	3eqtrd 2860	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍)))
174	165, 173	jca 514	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
175		eqidd 2822	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → 𝑅 = 𝑅)
176		simpl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → 𝑒 = (𝑐 ↾ 𝑅))
177	176	fveq1d 6666	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → (𝑒‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
178	175, 177	sumeq12rdv 15058	. . . . . . . . . . . . . 14 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡))
179	178	eqeq1d 2823	. . . . . . . . . . . . 13 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍)) ↔ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
180	179	elrab 3679	. . . . . . . . . . . 12 ⊢ ((𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ↔ ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
181	174, 180	sylibr 236	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
182		oveq2 7158	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑅 → ((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m 𝑅))
183		rabeq 3483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑛) ↑_m 𝑠) = ((0...𝑛) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
184	182, 183	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
185		sumeq1 15039	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑅 → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
186	185	eqeq1d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑅 → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛))
187	186	rabbidv 3480	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
188	184, 187	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
189	188	mpteq2dv 5154	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑅 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
190		elpwg 4544	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇 ↔ 𝑅 ⊆ 𝑇))
191	162, 190	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ∈ 𝒫 𝑇 ↔ 𝑅 ⊆ 𝑇))
192	108, 191	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ 𝒫 𝑇)
193	24	mptex 6980	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V
194	193	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V)
195	8, 189, 192, 194	fvmptd3 6785	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
196	195	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
197		oveq2 7158	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
198	197	oveq1d 7165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((0...𝑛) ↑_m 𝑅) = ((0...𝑚) ↑_m 𝑅))
199		rabeq 3483	. . . . . . . . . . . . . . . . . 18 ⊢ (((0...𝑛) ↑_m 𝑅) = ((0...𝑚) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
200	198, 199	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
201		eqeq2 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚))
202	201	rabbidv 3480	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
203	200, 202	eqtrd 2856	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
204	203	cbvmptv 5161	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
205	204	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
206	196, 205	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
207		fveq1 6663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑡) = (𝑒‘𝑡))
208	207	sumeq2sdv 15055	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑒 → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑒‘𝑡))
209	208	eqeq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚))
210	209	cbvrabv 3491	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚}
211	210	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
212		oveq2 7158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐‘𝑍))))
213	212	oveq1d 7165	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → ((0...𝑚) ↑_m 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅))
214		rabeq 3483	. . . . . . . . . . . . . . . 16 ⊢ (((0...𝑚) ↑_m 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) → {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
215	213, 214	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
216		eqeq2 2833	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))))
217	216	rabbidv 3480	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
218	211, 215, 217	3eqtrd 2860	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
219	218	adantl 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑚 = (𝐽 − (𝑐‘𝑍))) → {𝑐 ∈ ((0...𝑚) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
220	56, 63	jca 514	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
221		elnn0z 11988	. . . . . . . . . . . . . 14 ⊢ ((𝐽 − (𝑐‘𝑍)) ∈ ℕ₀ ↔ ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
222	220, 221	sylibr 236	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℕ₀)
223		ovex 7183	. . . . . . . . . . . . . . 15 ⊢ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∈ V
224	223	rabex 5227	. . . . . . . . . . . . . 14 ⊢ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V
225	224	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V)
226	206, 219, 222, 225	fvmptd 6769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
227	226	eqcomd 2827	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
228	181, 227	eleqtrd 2915	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
229	70, 228	jca 514	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
230	1, 229	jca 514	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
231		ovexd 7185	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ V)
232		vex 3497	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
233	232	resex 5893	. . . . . . . . . 10 ⊢ (𝑐 ↾ 𝑅) ∈ V
234	233	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ V)
235		opeq12 4798	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
236	235	eqeq2d 2832	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
237		eleq1 2900	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
238	237	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
239		simpr 487	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → 𝑑 = (𝑐 ↾ 𝑅))
240		fveq2 6664	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
241	240	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
242	239, 241	eleq12d 2907	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑑 ∈ ((𝐶‘𝑅)‘𝑘) ↔ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
243	238, 242	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
244	236, 243	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))))
245	244	spc2egv 3599	. . . . . . . . 9 ⊢ (((𝐽 − (𝑐‘𝑍)) ∈ V ∧ (𝑐 ↾ 𝑅) ∈ V) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
246	231, 234, 245	syl2anc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
247	230, 246	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
248		eliunxp 5702	. . . . . . 7 ⊢ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
249	247, 248	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
250		dvnprodlem1.d	. . . . . 6 ⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
251	249, 250	fmptd 6872	. . . . 5 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
252	93	nfcri 2971	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
253	94, 252	nfan 1896	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
254	77, 253	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
255		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝐷‘𝑐) = (𝐷‘𝑒)
256	254, 255	nfan 1896	. . . . . . . . 9 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒))
257	97	eqcomd 2827	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
258	257	adantlrr 719	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
259	258	adantlr 713	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
260	250	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
261		opex 5348	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V
262	261	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V)
263	260, 262	fvmpt2d 6775	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
264	263	fveq2d 6668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
265	264	fveq1d 6666	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡))
266		ovex 7183	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 − (𝑐‘𝑍)) ∈ V
267	266, 233	op2nd 7692	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝑐 ↾ 𝑅)
268	267	fveq1i 6665	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡)
269	268	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
270	265, 269	eqtr2d 2857	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
271	270	adantrr 715	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
272	271	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
273		simpr 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = (𝐷‘𝑒))
274		fveq1 6663	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑍) = (𝑒‘𝑍))
275	274	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝑒‘𝑍)))
276		reseq1 5841	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (𝑐 ↾ 𝑅) = (𝑒 ↾ 𝑅))
277	275, 276	opeq12d 4804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
278		simpr 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
279		opex 5348	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V
280	279	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V)
281	250, 277, 278, 280	fvmptd3 6785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
282	281	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
283	273, 282	eqtrd 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
284	283	fveq2d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
285	284	adantlrl 718	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
286	285	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
287		ovex 7183	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 − (𝑒‘𝑍)) ∈ V
288		vex 3497	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑒 ∈ V
289	288	resex 5893	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ↾ 𝑅) ∈ V
290	287, 289	op2nd 7692	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅)
291	290	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅))
292	286, 291	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘(𝐷‘𝑐)) = (𝑒 ↾ 𝑅))
293	292	fveq1d 6666	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = ((𝑒 ↾ 𝑅)‘𝑡))
294		fvres 6683	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝑅 → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
295	294	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
296	293, 295	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = (𝑒‘𝑡))
297	259, 272, 296	3eqtrd 2860	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
298	297	adantlr 713	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
299		simpl 485	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
300		elunnel1 4125	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 ∈ {𝑍})
301		elsni 4577	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
302	300, 301	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
303	302	adantll 712	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
304		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
305	304	fveq2d 6668	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑐‘𝑍))
306	3	nn0cnd 11951	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ ℂ)
307	306	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
308	307, 129	nncand 10996	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝑐‘𝑍))
309	308	eqcomd 2827	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
310	309	adantrr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
311	310	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
312	263	fveq2d 6668	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
313	266, 233	op1st 7691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍))
314	313	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍)))
315	312, 314	eqtr2d 2857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) = (1^st ‘(𝐷‘𝑐)))
316	315	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
317	316	adantrr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
318	317	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
319		fveq2 6664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷‘𝑐) = (𝐷‘𝑒) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘(𝐷‘𝑒)))
320	319	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘(𝐷‘𝑒)))
321	281	fveq2d 6668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘(𝐷‘𝑒)) = (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
322	321	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑒)) = (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
323	287, 289	op1st 7691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍))
324	323	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍)))
325	320, 322, 324	3eqtrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑐)) = (𝐽 − (𝑒‘𝑍)))
326	325	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝐽 − (𝐽 − (𝑒‘𝑍))))
327	306	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
328		zsscn 11983	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℤ ⊆ ℂ
329	6, 328	sstri 3975	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0...𝐽) ⊆ ℂ
330	329	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
331		eleq1w 2895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
332	331	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
333		feq1 6489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
334	332, 333	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
335	334, 47	chvarvv 2001	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
336	52	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
337	335, 336	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ (0...𝐽))
338	330, 337	sseldd 3967	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ ℂ)
339	327, 338	nncand 10996	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
340	339	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
341		eqidd 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑒‘𝑍) = (𝑒‘𝑍))
342	326, 340, 341	3eqtrd 2860	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
343	342	adantlrl 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
344	311, 318, 343	3eqtrd 2860	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝑒‘𝑍))
345	344	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑍) = (𝑒‘𝑍))
346		fveq2 6664	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑡) = (𝑒‘𝑍))
347	346	eqcomd 2827	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑍) = (𝑒‘𝑡))
348	347	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑒‘𝑍) = (𝑒‘𝑡))
349	305, 345, 348	3eqtrd 2860	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
350	349	adantlr 713	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
351	299, 303, 350	syl2anc 586	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
352	298, 351	pm2.61dan 811	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐‘𝑡) = (𝑒‘𝑡))
353	352	ex 415	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → (𝑐‘𝑡) = (𝑒‘𝑡)))
354	256, 353	ralrimi 3216	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡))
355	72	adantrr 715	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
356	355	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
357	335	ffnd 6509	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
358	357	adantrl 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
359	358	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
360		eqfnfv 6796	. . . . . . . . 9 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
361	356, 359, 360	syl2anc 586	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
362	354, 361	mpbird 259	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 = 𝑒)
363	362	ex 415	. . . . . 6 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
364	363	ralrimivva 3191	. . . . 5 ⊢ (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
365	251, 364	jca 514	. . . 4 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
366		dff13 7007	. . . 4 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
367	365, 366	sylibr 236	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
368		eliun 4915	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
369	368	biimpi 218	. . . . . . . . . 10 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
370	369	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
371		nfv 1911	. . . . . . . . . . 11 ⊢ Ⅎ𝑘𝜑
372		nfcv 2977	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝑝
373		nfiu1 4945	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
374	372, 373	nfel 2992	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
375	371, 374	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
376		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}
377		nfv 1911	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑘 ∈ (0...𝐽)
378		nfcv 2977	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑝
379		nfcv 2977	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑘}
380		nfcv 2977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡𝑅
381	89, 380	nffv 6674	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝐶‘𝑅)
382		nfcv 2977	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝑘
383	381, 382	nffv 6674	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝐶‘𝑅)‘𝑘)
384	379, 383	nfxp 5582	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡({𝑘} × ((𝐶‘𝑅)‘𝑘))
385	378, 384	nfel 2992	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))
386	77, 377, 385	nf3an 1898	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
387		0zd 11987	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
388	4	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
389	388	3ad2antl1 1181	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
390		iftrue 4472	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ 𝑅 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
391	390	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
392		fzssz 12903	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0...𝑘) ⊆ ℤ
393	392	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → (0...𝑘) ⊆ ℤ)
394		simp1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝜑)
395		simp2 1133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
396		xp2nd 7716	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (2^nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
397	396	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
398	195	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
399		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
400	399	oveq1d 7165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑘 → ((0...𝑛) ↑_m 𝑅) = ((0...𝑘) ↑_m 𝑅))
401		rabeq 3483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((0...𝑛) ↑_m 𝑅) = ((0...𝑘) ↑_m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
402	400, 401	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
403		eqeq2 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑘 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘))
404	403	rabbidv 3480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
405	402, 404	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
406	405	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
407		elfznn0 12994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ₀)
408	407	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ₀)
409		ovex 7183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((0...𝑘) ↑_m 𝑅) ∈ V
410	409	rabex 5227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V
411	410	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V)
412	398, 406, 408, 411	fvmptd 6769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
413	412	3adant3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
414	397, 413	eleqtrd 2915	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
415		elrabi 3674	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
416	415	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ (2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘}) → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
417	394, 395, 414, 416	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅))
418		elmapi 8422	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
419	417, 418	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
420	419	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
421	420	ffvelrnda 6845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
422	393, 421	sseldd 3967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
423	391, 422	eqeltrd 2913	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
424		simpl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
425	302	adantll 712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
426		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
427	134	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
428	426, 427	eqneltrd 2932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
429	428	iffalsed 4477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
430	429	3ad2antl1 1181	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
431	4	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
432	431	3ad2antl1 1181	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
433		xp1st 7715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ {𝑘})
434		elsni 4577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((1^st ‘𝑝) ∈ {𝑘} → (1^st ‘𝑝) = 𝑘)
435	433, 434	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) = 𝑘)
436	435	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) = 𝑘)
437	6	sseli 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
438	437	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
439	436, 438	eqeltrd 2913	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ ℤ)
440	439	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ ℤ)
441	440	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1^st ‘𝑝) ∈ ℤ)
442	432, 441	zsubcld 12086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1^st ‘𝑝)) ∈ ℤ)
443	430, 442	eqeltrd 2913	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
444	443	adantlr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
445	424, 425, 444	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
446	423, 445	pm2.61dan 811	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
447	387, 389, 446	3jca 1124	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ))
448	419	ffvelrnda 6845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
449		elfzle1 12904	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2^nd ‘𝑝)‘𝑡))
450	448, 449	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ ((2^nd ‘𝑝)‘𝑡))
451	390	eqcomd 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ 𝑅 → ((2^nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
452	451	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
453	450, 452	breqtrd 5084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
454	453	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
455		simpll 765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))))
456		elfzle2 12905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ≤ 𝐽)
457		elfzel2 12900	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
458	457	zred 12081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
459	113	sseli 3962	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
460	458, 459	subge0d 11224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽 − 𝑘) ↔ 𝑘 ≤ 𝐽))
461	456, 460	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽 − 𝑘))
462	461	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
463	462	3ad2antl2 1182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
464	394, 428	sylan 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
465	464	iffalsed 4477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
466	436	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) = 𝑘)
467	466	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) = (𝐽 − 𝑘))
468	467	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1^st ‘𝑝)) = (𝐽 − 𝑘))
469	465, 468	eqtr2d 2857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
470	463, 469	breqtrd 5084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
471	455, 425, 470	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
472	454, 471	pm2.61dan 811	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
473		simpl2 1188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 𝑘 ∈ (0...𝐽))
474	392	sseli 3962	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
475	474	zred 12081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ∈ ℝ)
476	475	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ∈ ℝ)
477	459	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
478	458	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
479		elfzle2 12905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝑘)
480	479	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝑘)
481	456	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ≤ 𝐽)
482	476, 477, 478, 480, 481	letrd 10791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
483	448, 473, 482	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
484	483	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
485	391, 484	eqbrtrd 5080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
486	469	eqcomd 2827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − 𝑘))
487	408	nn0ge0d 11952	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
488	458	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
489	459	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
490	488, 489	subge02d 11226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽 − 𝑘) ≤ 𝐽))
491	487, 490	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐽 − 𝑘) ≤ 𝐽)
492	491	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
493	492	3adantl3 1164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
494	486, 493	eqbrtrd 5080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
495	455, 425, 494	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
496	485, 495	pm2.61dan 811	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
497	447, 472, 496	jca32 518	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∧ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)))
498		elfz2 12893	. . . . . . . . . . . . . . . . 17 ⊢ (if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∧ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)))
499	497, 498	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ (0...𝐽))
500		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
501	386, 499, 500	fmptdf 6875	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
502		ovexd 7185	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (0...𝐽) ∈ V)
503	394, 20	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
504	502, 503	elmapd 8414	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ↔ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽)))
505	501, 504	mpbird 259	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})))
506		eqidd 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
507		eleq1w 2895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑡 → (𝑟 ∈ 𝑅 ↔ 𝑡 ∈ 𝑅))
508		fveq2 6664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑡 → ((2^nd ‘𝑝)‘𝑟) = ((2^nd ‘𝑝)‘𝑡))
509	507, 508	ifbieq1d 4489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑡 → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
510	509	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑟 = 𝑡) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
511		simpr 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
512	506, 510, 511, 446	fvmptd 6769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
513	512	ex 415	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
514	386, 513	ralrimi 3216	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
515	514	sumeq2d 15053	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
516		nfcv 2977	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))
517	394, 110	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑅 ∈ Fin)
518	394, 48	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑍 ∈ 𝑇)
519	394, 134	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ¬ 𝑍 ∈ 𝑅)
520	390	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
521	448, 474	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
522	521	zcnd 12082	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℂ)
523	520, 522	eqeltrd 2913	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℂ)
524		eleq1 2900	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑍 → (𝑡 ∈ 𝑅 ↔ 𝑍 ∈ 𝑅))
525		fveq2 6664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑍 → ((2^nd ‘𝑝)‘𝑡) = ((2^nd ‘𝑝)‘𝑍))
526	524, 525	ifbieq1d 4489	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))))
527	134	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ¬ 𝑍 ∈ 𝑅)
528	527	iffalsed 4477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
529	528	3adant2 1127	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
530	4	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
531	530, 440	zsubcld 12086	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) ∈ ℤ)
532	531	zcnd 12082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) ∈ ℂ)
533	529, 532	eqeltrd 2913	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) ∈ ℂ)
534	386, 516, 517, 518, 519, 523, 526, 533	fsumsplitsn 15094	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))))
535	390	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡)))
536	386, 535	ralrimi 3216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
537	536	sumeq2d 15053	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡))
538		eqidd 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (2^nd ‘𝑝) → 𝑅 = 𝑅)
539		simpl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐 = (2^nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → 𝑐 = (2^nd ‘𝑝))
540	539	fveq1d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 = (2^nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((2^nd ‘𝑝)‘𝑡))
541	538, 540	sumeq12rdv 15058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = (2^nd ‘𝑝) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡))
542	541	eqeq1d 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (2^nd ‘𝑝) → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘 ↔ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
543	542	elrab 3679	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ↔ ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
544	414, 543	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
545	544	simprd 498	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘)
546	537, 545	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = 𝑘)
547	519	iffalsed 4477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
548	547, 467	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − 𝑘))
549	546, 548	oveq12d 7168	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))) = (𝑘 + (𝐽 − 𝑘)))
550	329	sseli 3962	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
551	550	3ad2ant2 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
552	394, 306	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
553	551, 552	pncan3d 10994	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 + (𝐽 − 𝑘)) = 𝐽)
554	549, 553	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))) = 𝐽)
555	515, 534, 554	3eqtrd 2860	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽)
556	505, 555	jca 514	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
557		eleq1w 2895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑟 → (𝑡 ∈ 𝑅 ↔ 𝑟 ∈ 𝑅))
558		fveq2 6664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑟 → ((2^nd ‘𝑝)‘𝑡) = ((2^nd ‘𝑝)‘𝑟))
559	557, 558	ifbieq1d 4489	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑟 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))
560	559	cbvmptv 5161	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))
561	560	eqeq2i 2834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
562	561	biimpi 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
563		fveq1 6663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) → (𝑐‘𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡))
564	563	sumeq2sdv 15055	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡))
565	562, 564	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡))
566	565	eqeq1d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
567	566	elrab 3679	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ↔ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
568	556, 567	sylibr 236	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
569	568	3exp 1115	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
570	569	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
571	375, 376, 570	rexlimd 3317	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}))
572	370, 571	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
573	39	eqcomd 2827	. . . . . . . . 9 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
574	573	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑_m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
575	572, 574	eleqtrd 2915	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
576	250	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
577		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
578	560	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
579	577, 578	eqtrd 2856	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
580		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → 𝑟 = 𝑍)
581	134	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
582	580, 581	eqneltrd 2932	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑟 ∈ 𝑅)
583	582	iffalsed 4477	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
584	583	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
585	52	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
586		ovexd 7185	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (1^st ‘𝑝)) ∈ V)
587	579, 584, 585, 586	fvmptd 6769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐‘𝑍) = (𝐽 − (1^st ‘𝑝)))
588	587	oveq2d 7166	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1^st ‘𝑝))))
589	588	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1^st ‘𝑝))))
590	306	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝐽 ∈ ℂ)
591		nfv 1911	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(1^st ‘𝑝) ∈ (0...𝐽)
592		simpl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
593		simpr 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → (1^st ‘𝑝) = 𝑘)
594		simpl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → 𝑘 ∈ (0...𝐽))
595	593, 594	eqeltrd 2913	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → (1^st ‘𝑝) ∈ (0...𝐽))
596	592, 436, 595	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ (0...𝐽))
597	596	ex 415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽)))
598	597	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽))))
599	374, 591, 598	rexlimd 3317	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽)))
600	369, 599	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽))
601	6	sseli 3962	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑝) ∈ (0...𝐽) → (1^st ‘𝑝) ∈ ℤ)
602	600, 601	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ ℤ)
603	602	zcnd 12082	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ ℂ)
604	603	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (1^st ‘𝑝) ∈ ℂ)
605	590, 604	nncand 10996	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝐽 − (1^st ‘𝑝))) = (1^st ‘𝑝))
606	589, 605	eqtrd 2856	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (1^st ‘𝑝))
607		reseq1 5841	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (𝑐 ↾ 𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅))
608	607	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐 ↾ 𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅))
609	73	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
610	609	resmptd 5902	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅) = (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
611		nfv 1911	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝)
612	390	mpteq2ia 5149	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡))
613	612	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡)))
614	419	feqmptd 6727	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡)))
615	613, 614	eqtr4d 2859	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
616	615	3exp 1115	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))))
617	616	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))))
618	375, 611, 617	rexlimd 3317	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝)))
619	370, 618	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
620	619	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
621	608, 610, 620	3eqtrd 2860	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐 ↾ 𝑅) = (2^nd ‘𝑝))
622	606, 621	opeq12d 4804	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
623		opex 5348	. . . . . . . . . 10 ⊢ ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ ∈ V
624	623	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ ∈ V)
625	576, 622, 575, 624	fvmptd 6769	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
626		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑘⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝
627		1st2nd2 7722	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → 𝑝 = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
628	627	eqcomd 2827	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝)
629	628	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝))
630	629	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝)))
631	375, 626, 630	rexlimd 3317	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝))
632	370, 631	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝)
633	625, 632	eqtr2d 2857	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))))
634		fveq2 6664	. . . . . . . 8 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (𝐷‘𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))))
635	634	rspceeqv 3637	. . . . . . 7 ⊢ (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
636	575, 633, 635	syl2anc 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
637	636	ralrimiva 3182	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
638	251, 637	jca 514	. . . 4 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
639		dffo3 6862	. . . 4 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
640	638, 639	sylibr 236	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
641	367, 640	jca 514	. 2 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))))
642		df-f1o 6356	. 2 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))))
643	641, 642	sylibr 236	1 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∃wex 1776 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 {crab 3142 Vcvv 3494 ∪ cun 3933 ⊆ wss 3935 ifcif 4466 𝒫 cpw 4538 {csn 4560 ⟨cop 4566 ∪ ciun 4911 class class class wbr 5058 ↦ cmpt 5138 × cxp 5547 ↾ cres 5551 Fn wfn 6344 ⟶wf 6345 –1-1→wf1 6346 –onto→wfo 6347 –1-1-onto→wf1o 6348 ‘cfv 6349 (class class class)co 7150 1^st c1st 7681 2^nd c2nd 7682 ↑_m cmap 8400 Fincfn 8503 ℂcc 10529 ℝcr 10530 0cc0 10531 + caddc 10534 ≤ cle 10670 − cmin 10864 ℕ₀cn0 11891 ℤcz 11975 ...cfz 12886 Σcsu 15036

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-se 5509 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-isom 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-sup 8900 df-oi 8968 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-rp 12384 df-ico 12738 df-fz 12887 df-fzo 13028 df-seq 13364 df-exp 13424 df-hash 13685 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-clim 14839 df-sum 15037

This theorem is referenced by: dvnprodlem2 42225

W3C validator