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 41103

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

**Hypotheses**
Ref	Expression
dvnprodlem1.c	⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
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 2779	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
2		0zd 11745	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3		dvnprodlem1.j	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
4	3	nn0zd 11837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ ℤ)
5	4	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6		fzssz 12665	. . . . . . . . . . . . . . . 16 ⊢ (0...𝐽) ⊆ ℤ
7	6	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℤ)
8		dvnprodlem1.c	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
9		oveq2 6932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑_𝑚 𝑠) = ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})))
10		rabeq 3389	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((0...𝑛) ↑_𝑚 𝑠) = ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
11	9, 10	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
12		sumeq1 14836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
13	12	eqeq1d 2780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛))
14	13	rabbidv 3386	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
15	11, 14	eqtrd 2814	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
16	15	mpteq2dv 4982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
17		dvnprodlem1.rzt	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
18		dvnprodlem1.t	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑇 ∈ Fin)
19		ssexg 5043	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∪ {𝑍}) ⊆ 𝑇 ∧ 𝑇 ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ V)
20	17, 18, 19	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
21		elpwg 4387	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
23	17, 22	mpbird 249	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
24		nn0ex 11654	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ₀ ∈ V
25	24	mptex 6760	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V
26	25	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V)
27	8, 16, 23, 26	fvmptd3 6566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
28		oveq2 6932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
29	28	oveq1d 6939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝐽 → ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})))
30		rabeq 3389	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
32		eqeq2 2789	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
33	32	rabbidv 3386	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
34	31, 33	eqtrd 2814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
35	34	adantl 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
36		ovex 6956	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∈ V
37	36	rabex 5051	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V)
39	27, 35, 3, 38	fvmptd 6550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
40		ssrab2 3908	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍}))
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})))
42	39, 41	eqsstrd 3858	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})))
43	42	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})))
44		simpr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
45	43, 44	sseldd 3822	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})))
46		elmapi 8164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
47	45, 46	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
48		dvnprodlem1.z	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑍 ∈ 𝑇)
49		snidg 4428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑍 ∈ 𝑇 → 𝑍 ∈ {𝑍})
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
51		elun2 4004	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
52	50, 51	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ (𝑅 ∪ {𝑍}))
53	52	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
54	47, 53	ffvelrnd 6626	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ (0...𝐽))
55	7, 54	sseldd 3822	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℤ)
56	5, 55	zsubcld 11844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
57	2, 5, 56	3jca 1119	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ))
58		elfzle2 12667	. . . . . . . . . . . . . 14 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → (𝑐‘𝑍) ≤ 𝐽)
59	54, 58	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ≤ 𝐽)
60	5	zred 11839	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
61	55	zred 11839	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℝ)
62	60, 61	subge0d 10968	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐‘𝑍)) ↔ (𝑐‘𝑍) ≤ 𝐽))
63	59, 62	mpbird 249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐‘𝑍)))
64		elfzle1 12666	. . . . . . . . . . . . . 14 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑍))
65	54, 64	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐‘𝑍))
66	60, 61	subge02d 10970	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐‘𝑍) ↔ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽))
67	65, 66	mpbid 224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)
68	57, 63, 67	jca32 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐‘𝑍)) ∧ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)))
69		elfz2 12655	. . . . . . . . . . 11 ⊢ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐‘𝑍)) ∧ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)))
70	68, 69	sylibr 226	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽))
71		elmapfn 8165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
72	45, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
73		ssun1 3999	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 ⊆ (𝑅 ∪ {𝑍})
74	73	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
75		fnssres 6252	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑅 ⊆ (𝑅 ∪ {𝑍})) → (𝑐 ↾ 𝑅) Fn 𝑅)
76	72, 74, 75	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) Fn 𝑅)
77		nfv 1957	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝜑
78		nfcv 2934	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡𝑐
79		nfcv 2934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡𝒫 𝑇
80		nfcv 2934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡ℕ₀
81		nfcv 2934	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡𝑠
82	81	nfsum1 14837	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡)
83		nfcv 2934	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡𝑛
84	82, 83	nfeq 2945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛
85		nfcv 2934	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡((0...𝑛) ↑_𝑚 𝑠)
86	84, 85	nfrab 3310	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡{𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}
87	80, 86	nfmpt 4983	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
88	79, 87	nfmpt 4983	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
89	8, 88	nfcxfr 2932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡𝐶
90		nfcv 2934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡(𝑅 ∪ {𝑍})
91	89, 90	nffv 6458	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝐶‘(𝑅 ∪ {𝑍}))
92		nfcv 2934	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐽
93	91, 92	nffv 6458	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
94	78, 93	nfel 2946	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
95	77, 94	nfan 1946	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
96		fvres 6467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
97	96	adantl 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
98	2	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ∈ ℤ)
99	56	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
100	6	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (0...𝐽) ⊆ ℤ)
101	47	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
102	74	sselda 3821	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
103	101, 102	ffvelrnd 6626	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...𝐽))
104	100, 103	sseldd 3822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ ℤ)
105	98, 99, 104	3jca 1119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (0 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ (𝑐‘𝑡) ∈ ℤ))
106		elfzle1 12666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐‘𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑡))
107	103, 106	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ≤ (𝑐‘𝑡))
108	17	unssad 4013	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑅 ⊆ 𝑇)
109		ssfi 8470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑇 ∈ Fin ∧ 𝑅 ⊆ 𝑇) → 𝑅 ∈ Fin)
110	18, 108, 109	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ∈ Fin)
111	110	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑅 ∈ Fin)
112		zssre 11740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℤ ⊆ ℝ
113	6, 112	sstri 3830	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0...𝐽) ⊆ ℝ
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (0...𝐽) ⊆ ℝ)
115	47	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
116	74	sselda 3821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
117	115, 116	ffvelrnd 6626	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ (0...𝐽))
118	114, 117	sseldd 3822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
119	118	adantlr 705	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
120		elfzle1 12666	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑟))
121	117, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
122	121	adantlr 705	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
123		fveq2 6448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 = 𝑡 → (𝑐‘𝑟) = (𝑐‘𝑡))
124		simpr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ 𝑅)
125	111, 119, 122, 123, 124	fsumge1 14942	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
126	110	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
127	118	recnd 10407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℂ)
128	126, 127	fsumcl 14880	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) ∈ ℂ)
129	61	recnd 10407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℂ)
130	128, 129	pncand 10737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) − (𝑐‘𝑍)) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
131		nfv 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑟(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
132		nfcv 2934	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑟(𝑐‘𝑍)
133	48	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ 𝑇)
134		dvnprodlem1.zr	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑅)
135	134	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍 ∈ 𝑅)
136		fveq2 6448	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑟 = 𝑍 → (𝑐‘𝑟) = (𝑐‘𝑍))
137	131, 132, 126, 133, 135, 127, 136, 129	fsumsplitsn 14890	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)))
138	137	eqcomd 2784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟))
139	123	cbvsumv 14843	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡)
140	139	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
141	39	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
142	44, 141	eleqtrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
143		rabid 3302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
144	142, 143	sylib 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
145	144	simprd 491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽)
146	140, 145	eqtrd 2814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = 𝐽)
147	138, 146	eqtrd 2814	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = 𝐽)
148	147	oveq1d 6939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) − (𝑐‘𝑍)) = (𝐽 − (𝑐‘𝑍)))
149	130, 148	eqtr3d 2816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
150	149	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
151	125, 150	breqtrd 4914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))
152	105, 107, 151	jca32 511	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((0 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ (𝑐‘𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐‘𝑡) ∧ (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))))
153		elfz2 12655	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))) ↔ ((0 ∈ ℤ ∧ (𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ (𝑐‘𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐‘𝑡) ∧ (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))))
154	152, 153	sylibr 226	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
155	97, 154	eqeltrd 2859	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
156	155	ex 403	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
157	95, 156	ralrimi 3139	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
158	76, 157	jca 507	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
159		ffnfv 6654	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))) ↔ ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
160	158, 159	sylibr 226	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))))
161		ovexd 6958	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐‘𝑍))) ∈ V)
162	18, 108	ssexd 5044	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ V)
163	162	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ V)
164	161, 163	elmapd 8156	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ↔ (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍)))))
165	160, 164	mpbird 249	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅))
166	96	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡)))
167	95, 166	ralrimi 3139	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
168	167	sumeq2d 14849	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
169	123	cbvsumv 14843	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡)
170	169	eqcomi 2787	. . . . . . . . . . . . . . 15 ⊢ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟)
171	170	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
172	149	idi 2	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
173	168, 171, 172	3eqtrd 2818	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍)))
174	165, 173	jca 507	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
175		eqidd 2779	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → 𝑅 = 𝑅)
176		simpl 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → 𝑒 = (𝑐 ↾ 𝑅))
177	176	fveq1d 6450	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → (𝑒‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
178	175, 177	sumeq12rdv 14854	. . . . . . . . . . . . . 14 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡))
179	178	eqeq1d 2780	. . . . . . . . . . . . 13 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍)) ↔ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
180	179	elrab 3572	. . . . . . . . . . . 12 ⊢ ((𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ↔ ((𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
181	174, 180	sylibr 226	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
182		oveq2 6932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑅 → ((0...𝑛) ↑_𝑚 𝑠) = ((0...𝑛) ↑_𝑚 𝑅))
183		rabeq 3389	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑛) ↑_𝑚 𝑠) = ((0...𝑛) ↑_𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
184	182, 183	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
185		sumeq1 14836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑅 → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
186	185	eqeq1d 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑅 → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛))
187	186	rabbidv 3386	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
188	184, 187	eqtrd 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
189	188	mpteq2dv 4982	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑅 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
190		elpwg 4387	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇 ↔ 𝑅 ⊆ 𝑇))
191	162, 190	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ∈ 𝒫 𝑇 ↔ 𝑅 ⊆ 𝑇))
192	108, 191	mpbird 249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ 𝒫 𝑇)
193	24	mptex 6760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V
194	193	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V)
195	8, 189, 192, 194	fvmptd3 6566	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
196	195	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
197		oveq2 6932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
198	197	oveq1d 6939	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → ((0...𝑛) ↑_𝑚 𝑅) = ((0...𝑚) ↑_𝑚 𝑅))
199		rabeq 3389	. . . . . . . . . . . . . . . . . 18 ⊢ (((0...𝑛) ↑_𝑚 𝑅) = ((0...𝑚) ↑_𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
200	198, 199	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
201		eqeq2 2789	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚))
202	201	rabbidv 3386	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
203	200, 202	eqtrd 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
204	203	cbvmptv 4987	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
205	204	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
206	196, 205	eqtrd 2814	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑚 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
207		fveq1 6447	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑡) = (𝑒‘𝑡))
208	207	sumeq2sdv 14851	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑒 → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑒‘𝑡))
209	208	eqeq1d 2780	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑒 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚))
210	209	cbvrabv 3396	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚}
211	210	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
212		oveq2 6932	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐‘𝑍))))
213	212	oveq1d 6939	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → ((0...𝑚) ↑_𝑚 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅))
214		rabeq 3389	. . . . . . . . . . . . . . . 16 ⊢ (((0...𝑚) ↑_𝑚 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) → {𝑒 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
215	213, 214	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
216		eqeq2 2789	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))))
217	216	rabbidv 3386	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
218	211, 215, 217	3eqtrd 2818	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
219	218	adantl 475	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑚 = (𝐽 − (𝑐‘𝑍))) → {𝑐 ∈ ((0...𝑚) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
220	56, 63	jca 507	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
221		elnn0z 11746	. . . . . . . . . . . . . 14 ⊢ ((𝐽 − (𝑐‘𝑍)) ∈ ℕ₀ ↔ ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
222	220, 221	sylibr 226	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℕ₀)
223		ovex 6956	. . . . . . . . . . . . . . 15 ⊢ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∈ V
224	223	rabex 5051	. . . . . . . . . . . . . 14 ⊢ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V
225	224	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V)
226	206, 219, 222, 225	fvmptd 6550	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
227	226	eqcomd 2784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
228	181, 227	eleqtrd 2861	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
229	70, 228	jca 507	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
230	1, 229	jca 507	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
231		ovexd 6958	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ V)
232		vex 3401	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
233	232	resex 5695	. . . . . . . . . 10 ⊢ (𝑐 ↾ 𝑅) ∈ V
234	233	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ V)
235		opeq12 4640	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
236	235	eqeq2d 2788	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
237		eleq1 2847	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
238	237	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
239		simpr 479	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → 𝑑 = (𝑐 ↾ 𝑅))
240		fveq2 6448	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
241	240	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
242	239, 241	eleq12d 2853	. . . . . . . . . . . 12 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑑 ∈ ((𝐶‘𝑅)‘𝑘) ↔ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
243	238, 242	anbi12d 624	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
244	236, 243	anbi12d 624	. . . . . . . . . 10 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))))
245	244	spc2egv 3497	. . . . . . . . 9 ⊢ (((𝐽 − (𝑐‘𝑍)) ∈ V ∧ (𝑐 ↾ 𝑅) ∈ V) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
246	231, 234, 245	syl2anc 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
247	230, 246	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
248		eliunxp 5507	. . . . . . 7 ⊢ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
249	247, 248	sylibr 226	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
250		dvnprodlem1.d	. . . . . 6 ⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
251	249, 250	fmptd 6650	. . . . 5 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
252	93	nfcri 2929	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
253	94, 252	nfan 1946	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
254	77, 253	nfan 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
255		nfv 1957	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝐷‘𝑐) = (𝐷‘𝑒)
256	254, 255	nfan 1946	. . . . . . . . 9 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒))
257	97	eqcomd 2784	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
258	257	adantlrr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
259	258	adantlr 705	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
260	250	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
261		opex 5166	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V
262	261	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V)
263	260, 262	fvmpt2d 6556	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
264	263	fveq2d 6452	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
265	264	fveq1d 6450	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡))
266		ovex 6956	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 − (𝑐‘𝑍)) ∈ V
267	266, 233	op2nd 7456	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝑐 ↾ 𝑅)
268	267	fveq1i 6449	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡)
269	268	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2^nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
270	265, 269	eqtr2d 2815	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
271	270	adantrr 707	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
272	271	ad2antrr 716	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2^nd ‘(𝐷‘𝑐))‘𝑡))
273		simpr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = (𝐷‘𝑒))
274		fveq1 6447	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑍) = (𝑒‘𝑍))
275	274	oveq2d 6940	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝑒‘𝑍)))
276		reseq1 5638	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (𝑐 ↾ 𝑅) = (𝑒 ↾ 𝑅))
277	275, 276	opeq12d 4646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
278		simpr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
279		opex 5166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V
280	279	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V)
281	250, 277, 278, 280	fvmptd3 6566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
282	281	adantr 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
283	273, 282	eqtrd 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
284	283	fveq2d 6452	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
285	284	adantlrl 710	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
286	285	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘(𝐷‘𝑐)) = (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
287		ovex 6956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 − (𝑒‘𝑍)) ∈ V
288		vex 3401	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑒 ∈ V
289	288	resex 5695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ↾ 𝑅) ∈ V
290	287, 289	op2nd 7456	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅)
291	290	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅))
292	286, 291	eqtrd 2814	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2^nd ‘(𝐷‘𝑐)) = (𝑒 ↾ 𝑅))
293	292	fveq1d 6450	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = ((𝑒 ↾ 𝑅)‘𝑡))
294		fvres 6467	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝑅 → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
295	294	adantl 475	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
296	293, 295	eqtrd 2814	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘(𝐷‘𝑐))‘𝑡) = (𝑒‘𝑡))
297	259, 272, 296	3eqtrd 2818	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
298	297	adantlr 705	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
299		simpl 476	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
300		elunnel1 3977	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 ∈ {𝑍})
301		elsni 4415	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
302	300, 301	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
303	302	adantll 704	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
304		simpr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
305	304	fveq2d 6452	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑐‘𝑍))
306	3	nn0cnd 11709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ ℂ)
307	306	adantr 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
308	307, 129	nncand 10741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝑐‘𝑍))
309	308	eqcomd 2784	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
310	309	adantrr 707	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
311	310	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
312	263	fveq2d 6452	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
313	266, 233	op1st 7455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍))
314	313	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍)))
315	312, 314	eqtr2d 2815	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) = (1^st ‘(𝐷‘𝑐)))
316	315	oveq2d 6940	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
317	316	adantrr 707	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
318	317	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1^st ‘(𝐷‘𝑐))))
319		fveq2 6448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷‘𝑐) = (𝐷‘𝑒) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘(𝐷‘𝑒)))
320	319	adantl 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑐)) = (1^st ‘(𝐷‘𝑒)))
321	281	fveq2d 6452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1^st ‘(𝐷‘𝑒)) = (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
322	321	adantr 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑒)) = (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
323	287, 289	op1st 7455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍))
324	323	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍)))
325	320, 322, 324	3eqtrd 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1^st ‘(𝐷‘𝑐)) = (𝐽 − (𝑒‘𝑍)))
326	325	oveq2d 6940	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝐽 − (𝐽 − (𝑒‘𝑍))))
327	306	adantr 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
328		zsscn 11741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℤ ⊆ ℂ
329	6, 328	sstri 3830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0...𝐽) ⊆ ℂ
330	329	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
331		eleq1w 2842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
332	331	anbi2d 622	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
333		feq1 6274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
334	332, 333	imbi12d 336	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑒 → (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
335	334, 47	chvarv 2361	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
336	52	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
337	335, 336	ffvelrnd 6626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ (0...𝐽))
338	330, 337	sseldd 3822	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ ℂ)
339	327, 338	nncand 10741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
340	339	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
341		eqidd 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑒‘𝑍) = (𝑒‘𝑍))
342	326, 340, 341	3eqtrd 2818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
343	342	adantlrl 710	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1^st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
344	311, 318, 343	3eqtrd 2818	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝑒‘𝑍))
345	344	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑍) = (𝑒‘𝑍))
346		fveq2 6448	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑡) = (𝑒‘𝑍))
347	346	eqcomd 2784	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑍) = (𝑒‘𝑡))
348	347	adantl 475	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑒‘𝑍) = (𝑒‘𝑡))
349	305, 345, 348	3eqtrd 2818	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
350	349	adantlr 705	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
351	299, 303, 350	syl2anc 579	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
352	298, 351	pm2.61dan 803	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐‘𝑡) = (𝑒‘𝑡))
353	352	ex 403	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → (𝑐‘𝑡) = (𝑒‘𝑡)))
354	256, 353	ralrimi 3139	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡))
355	72	adantrr 707	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
356	355	adantr 474	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
357	335	ffnd 6294	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
358	357	adantrl 706	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
359	358	adantr 474	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
360		eqfnfv 6576	. . . . . . . . 9 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
361	356, 359, 360	syl2anc 579	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
362	354, 361	mpbird 249	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 = 𝑒)
363	362	ex 403	. . . . . 6 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
364	363	ralrimivva 3153	. . . . 5 ⊢ (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
365	251, 364	jca 507	. . . 4 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
366		dff13 6786	. . . 4 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
367	365, 366	sylibr 226	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
368		eliun 4759	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
369	368	biimpi 208	. . . . . . . . . 10 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
370	369	adantl 475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
371		nfv 1957	. . . . . . . . . . 11 ⊢ Ⅎ𝑘𝜑
372		nfcv 2934	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝑝
373		nfiu1 4785	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
374	372, 373	nfel 2946	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
375	371, 374	nfan 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
376		nfv 1957	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}
377		nfv 1957	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑘 ∈ (0...𝐽)
378		nfcv 2934	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑝
379		nfcv 2934	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑘}
380		nfcv 2934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡𝑅
381	89, 380	nffv 6458	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝐶‘𝑅)
382		nfcv 2934	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝑘
383	381, 382	nffv 6458	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡((𝐶‘𝑅)‘𝑘)
384	379, 383	nfxp 5390	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡({𝑘} × ((𝐶‘𝑅)‘𝑘))
385	378, 384	nfel 2946	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))
386	77, 377, 385	nf3an 1948	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
387		0zd 11745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
388	4	adantr 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
389	388	3ad2antl1 1193	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
390		iftrue 4313	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ 𝑅 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
391	390	adantl 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
392		fzssz 12665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0...𝑘) ⊆ ℤ
393	392	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → (0...𝑘) ⊆ ℤ)
394		simp1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝜑)
395		simp2 1128	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
396		xp2nd 7480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (2^nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
397	396	3ad2ant3 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
398	195	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
399		oveq2 6932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
400	399	oveq1d 6939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑘 → ((0...𝑛) ↑_𝑚 𝑅) = ((0...𝑘) ↑_𝑚 𝑅))
401		rabeq 3389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((0...𝑛) ↑_𝑚 𝑅) = ((0...𝑘) ↑_𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
402	400, 401	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
403		eqeq2 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑘 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘))
404	403	rabbidv 3386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
405	402, 404	eqtrd 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
406	405	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
407		elfznn0 12756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ₀)
408	407	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ₀)
409		ovex 6956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((0...𝑘) ↑_𝑚 𝑅) ∈ V
410	409	rabex 5051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V
411	410	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V)
412	398, 406, 408, 411	fvmptd 6550	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
413	412	3adant3 1123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
414	397, 413	eleqtrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
415		elrabi 3567	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_𝑚 𝑅))
416	415	3ad2ant3 1126	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ (2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘}) → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_𝑚 𝑅))
417	394, 395, 414, 416	syl3anc 1439	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) ∈ ((0...𝑘) ↑_𝑚 𝑅))
418		elmapi 8164	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_𝑚 𝑅) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
419	417, 418	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
420	419	adantr 474	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2^nd ‘𝑝):𝑅⟶(0...𝑘))
421	420	ffvelrnda 6625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
422	393, 421	sseldd 3822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
423	391, 422	eqeltrd 2859	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
424		simpl 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
425	302	adantll 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
426		simpr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
427	134	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
428	426, 427	eqneltrd 2878	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
429	428	iffalsed 4318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
430	429	3ad2antl1 1193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
431	4	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
432	431	3ad2antl1 1193	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
433		xp1st 7479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ {𝑘})
434		elsni 4415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((1^st ‘𝑝) ∈ {𝑘} → (1^st ‘𝑝) = 𝑘)
435	433, 434	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) = 𝑘)
436	435	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) = 𝑘)
437	6	sseli 3817	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
438	437	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
439	436, 438	eqeltrd 2859	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ ℤ)
440	439	3adant1 1121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ ℤ)
441	440	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1^st ‘𝑝) ∈ ℤ)
442	432, 441	zsubcld 11844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1^st ‘𝑝)) ∈ ℤ)
443	430, 442	eqeltrd 2859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
444	443	adantlr 705	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
445	424, 425, 444	syl2anc 579	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
446	423, 445	pm2.61dan 803	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ)
447	387, 389, 446	3jca 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ))
448	419	ffvelrnda 6625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
449		elfzle1 12666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2^nd ‘𝑝)‘𝑡))
450	448, 449	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ ((2^nd ‘𝑝)‘𝑡))
451	390	eqcomd 2784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ 𝑅 → ((2^nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
452	451	adantl 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
453	450, 452	breqtrd 4914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
454	453	adantlr 705	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
455		simpll 757	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))))
456		elfzle2 12667	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ≤ 𝐽)
457		elfzel2 12662	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
458	457	zred 11839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
459	113	sseli 3817	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
460	458, 459	subge0d 10968	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽 − 𝑘) ↔ 𝑘 ≤ 𝐽))
461	456, 460	mpbird 249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽 − 𝑘))
462	461	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
463	462	3ad2antl2 1194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
464	394, 428	sylan 575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
465	464	iffalsed 4318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
466	436	3adant1 1121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) = 𝑘)
467	466	oveq2d 6940	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) = (𝐽 − 𝑘))
468	467	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1^st ‘𝑝)) = (𝐽 − 𝑘))
469	465, 468	eqtr2d 2815	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
470	463, 469	breqtrd 4914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
471	455, 425, 470	syl2anc 579	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
472	454, 471	pm2.61dan 803	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
473		simpl2 1201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 𝑘 ∈ (0...𝐽))
474	392	sseli 3817	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
475	474	zred 11839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ∈ ℝ)
476	475	adantr 474	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ∈ ℝ)
477	459	adantl 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
478	458	adantl 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
479		elfzle2 12667	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝑘)
480	479	adantr 474	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝑘)
481	456	adantl 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ≤ 𝐽)
482	476, 477, 478, 480, 481	letrd 10535	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((2^nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
483	448, 473, 482	syl2anc 579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
484	483	adantlr 705	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ≤ 𝐽)
485	391, 484	eqbrtrd 4910	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
486	469	eqcomd 2784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = (𝐽 − 𝑘))
487	408	nn0ge0d 11710	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
488	458	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
489	459	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
490	488, 489	subge02d 10970	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽 − 𝑘) ≤ 𝐽))
491	487, 490	mpbid 224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐽 − 𝑘) ≤ 𝐽)
492	491	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
493	492	3adantl3 1170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
494	486, 493	eqbrtrd 4910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
495	455, 425, 494	syl2anc 579	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
496	485, 495	pm2.61dan 803	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)
497	447, 472, 496	jca32 511	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∧ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ≤ 𝐽)))
498		elfz2 12655	. . . . . . . . . . . . . . . . 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 226	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ (0...𝐽))
500		eqid 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
501	386, 499, 500	fmptdf 6653	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
502		ovexd 6958	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (0...𝐽) ∈ V)
503	394, 20	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
504	502, 503	elmapd 8156	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ↔ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽)))
505	501, 504	mpbird 249	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})))
506		eqidd 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
507		eleq1w 2842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑡 → (𝑟 ∈ 𝑅 ↔ 𝑡 ∈ 𝑅))
508		fveq2 6448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑡 → ((2^nd ‘𝑝)‘𝑟) = ((2^nd ‘𝑝)‘𝑡))
509	507, 508	ifbieq1d 4330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑡 → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
510	509	adantl 475	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑟 = 𝑡) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
511		simpr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
512	506, 510, 511, 446	fvmptd 6550	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
513	512	ex 403	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
514	386, 513	ralrimi 3139	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
515	514	sumeq2d 14849	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))
516		nfcv 2934	. . . . . . . . . . . . . . . 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 475	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
521	448, 474	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℤ)
522	521	zcnd 11840	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2^nd ‘𝑝)‘𝑡) ∈ ℂ)
523	520, 522	eqeltrd 2859	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) ∈ ℂ)
524		eleq1 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑍 → (𝑡 ∈ 𝑅 ↔ 𝑍 ∈ 𝑅))
525		fveq2 6448	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑍 → ((2^nd ‘𝑝)‘𝑡) = ((2^nd ‘𝑝)‘𝑍))
526	524, 525	ifbieq1d 4330	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))))
527	134	adantr 474	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ¬ 𝑍 ∈ 𝑅)
528	527	iffalsed 4318	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
529	528	3adant2 1122	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
530	4	3ad2ant1 1124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
531	530, 440	zsubcld 11844	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) ∈ ℤ)
532	531	zcnd 11840	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1^st ‘𝑝)) ∈ ℂ)
533	529, 532	eqeltrd 2859	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) ∈ ℂ)
534	386, 516, 517, 518, 519, 523, 526, 533	fsumsplitsn 14890	. . . . . . . . . . . . . . 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 3139	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = ((2^nd ‘𝑝)‘𝑡))
537	536	sumeq2d 14849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡))
538		eqidd 2779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (2^nd ‘𝑝) → 𝑅 = 𝑅)
539		simpl 476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐 = (2^nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → 𝑐 = (2^nd ‘𝑝))
540	539	fveq1d 6450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 = (2^nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((2^nd ‘𝑝)‘𝑡))
541	538, 540	sumeq12rdv 14854	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = (2^nd ‘𝑝) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡))
542	541	eqeq1d 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (2^nd ‘𝑝) → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘 ↔ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
543	542	elrab 3572	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑_𝑚 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ↔ ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_𝑚 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
544	414, 543	sylib 210	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((2^nd ‘𝑝) ∈ ((0...𝑘) ↑_𝑚 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘))
545	544	simprd 491	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 ((2^nd ‘𝑝)‘𝑡) = 𝑘)
546	537, 545	eqtrd 2814	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = 𝑘)
547	519	iffalsed 4318	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
548	547, 467	eqtrd 2814	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝))) = (𝐽 − 𝑘))
549	546, 548	oveq12d 6942	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))) = (𝑘 + (𝐽 − 𝑘)))
550	329	sseli 3817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
551	550	3ad2ant2 1125	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
552	394, 306	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
553	551, 552	pncan3d 10739	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 + (𝐽 − 𝑘)) = 𝐽)
554	549, 553	eqtrd 2814	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑍), (𝐽 − (1^st ‘𝑝)))) = 𝐽)
555	515, 534, 554	3eqtrd 2818	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽)
556	505, 555	jca 507	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
557		eleq1w 2842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑟 → (𝑡 ∈ 𝑅 ↔ 𝑟 ∈ 𝑅))
558		fveq2 6448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑟 → ((2^nd ‘𝑝)‘𝑡) = ((2^nd ‘𝑝)‘𝑟))
559	557, 558	ifbieq1d 4330	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑟 → if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))) = if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))
560	559	cbvmptv 4987	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))
561	560	eqeq2i 2790	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
562	561	biimpi 208	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
563		fveq1 6447	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))) → (𝑐‘𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡))
564	563	sumeq2sdv 14851	. . . . . . . . . . . . . . . 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 2780	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
567	566	elrab 3572	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ↔ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))))‘𝑡) = 𝐽))
568	556, 567	sylibr 226	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
569	568	3exp 1109	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
570	569	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
571	375, 376, 570	rexlimd 3208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}))
572	370, 571	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
573	39	eqcomd 2784	. . . . . . . . 9 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
574	573	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑_𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
575	572, 574	eleqtrd 2861	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
576	250	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
577		simpr 479	. . . . . . . . . . . . . . 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 2814	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝)))))
580		simpr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → 𝑟 = 𝑍)
581	134	adantr 474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
582	580, 581	eqneltrd 2878	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑟 ∈ 𝑅)
583	582	iffalsed 4318	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
584	583	adantlr 705	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑟), (𝐽 − (1^st ‘𝑝))) = (𝐽 − (1^st ‘𝑝)))
585	52	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
586		ovexd 6958	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (1^st ‘𝑝)) ∈ V)
587	579, 584, 585, 586	fvmptd 6550	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐‘𝑍) = (𝐽 − (1^st ‘𝑝)))
588	587	oveq2d 6940	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1^st ‘𝑝))))
589	588	adantlr 705	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1^st ‘𝑝))))
590	306	ad2antrr 716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → 𝐽 ∈ ℂ)
591		nfv 1957	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(1^st ‘𝑝) ∈ (0...𝐽)
592		simpl 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
593		simpr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → (1^st ‘𝑝) = 𝑘)
594		simpl 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → 𝑘 ∈ (0...𝐽))
595	593, 594	eqeltrd 2859	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (0...𝐽) ∧ (1^st ‘𝑝) = 𝑘) → (1^st ‘𝑝) ∈ (0...𝐽))
596	592, 436, 595	syl2anc 579	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1^st ‘𝑝) ∈ (0...𝐽))
597	596	ex 403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽)))
598	597	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽))))
599	374, 591, 598	rexlimd 3208	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽)))
600	369, 599	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ (0...𝐽))
601	6	sseli 3817	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑝) ∈ (0...𝐽) → (1^st ‘𝑝) ∈ ℤ)
602	600, 601	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ ℤ)
603	602	zcnd 11840	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1^st ‘𝑝) ∈ ℂ)
604	603	ad2antlr 717	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (1^st ‘𝑝) ∈ ℂ)
605	590, 604	nncand 10741	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝐽 − (1^st ‘𝑝))) = (1^st ‘𝑝))
606	589, 605	eqtrd 2814	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (1^st ‘𝑝))
607		reseq1 5638	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (𝑐 ↾ 𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅))
608	607	adantl 475	. . . . . . . . . . 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 5704	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ↾ 𝑅) = (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))
611		nfv 1957	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝)
612	390	mpteq2ia 4977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡))
613	612	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡)))
614	419	feqmptd 6511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2^nd ‘𝑝) = (𝑡 ∈ 𝑅 ↦ ((2^nd ‘𝑝)‘𝑡)))
615	613, 614	eqtr4d 2817	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
616	615	3exp 1109	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))))
617	616	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))))
618	375, 611, 617	rexlimd 3208	. . . . . . . . . . . . 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 474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) = (2^nd ‘𝑝))
621	608, 610, 620	3eqtrd 2818	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → (𝑐 ↾ 𝑅) = (2^nd ‘𝑝))
622	606, 621	opeq12d 4646	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
623		opex 5166	. . . . . . . . . 10 ⊢ ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ ∈ V
624	623	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ ∈ V)
625	576, 622, 575, 624	fvmptd 6550	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))) = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
626		nfv 1957	. . . . . . . . . 10 ⊢ Ⅎ𝑘⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝
627		1st2nd2 7486	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → 𝑝 = ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩)
628	627	eqcomd 2784	. . . . . . . . . . . 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 3208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝))
632	370, 631	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1^st ‘𝑝), (2^nd ‘𝑝)⟩ = 𝑝)
633	625, 632	eqtr2d 2815	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))))
634		fveq2 6448	. . . . . . . 8 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) → (𝐷‘𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝))))))
635	634	rspceeqv 3529	. . . . . . 7 ⊢ (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2^nd ‘𝑝)‘𝑡), (𝐽 − (1^st ‘𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
636	575, 633, 635	syl2anc 579	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
637	636	ralrimiva 3148	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
638	251, 637	jca 507	. . . 4 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
639		dffo3 6640	. . . 4 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
640	638, 639	sylibr 226	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
641	367, 640	jca 507	. 2 ⊢ (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))))
642		df-f1o 6144	. 2 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))))
643	641, 642	sylibr 226	1 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 386 ∧ w3a 1071 = wceq 1601 ∃wex 1823 ∈ wcel 2107 ∀wral 3090 ∃wrex 3091 {crab 3094 Vcvv 3398 ∪ cun 3790 ⊆ wss 3792 ifcif 4307 𝒫 cpw 4379 {csn 4398 ⟨cop 4404 ∪ ciun 4755 class class class wbr 4888 ↦ cmpt 4967 × cxp 5355 ↾ cres 5359 Fn wfn 6132 ⟶wf 6133 –1-1→wf1 6134 –onto→wfo 6135 –1-1-onto→wf1o 6136 ‘cfv 6137 (class class class)co 6924 1^st c1st 7445 2^nd c2nd 7446 ↑_𝑚 cmap 8142 Fincfn 8243 ℂcc 10272 ℝcr 10273 0cc0 10274 + caddc 10277 ≤ cle 10414 − cmin 10608 ℕ₀cn0 11647 ℤcz 11733 ...cfz 12648 Σcsu 14833

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5008 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228 ax-inf2 8837 ax-cnex 10330 ax-resscn 10331 ax-1cn 10332 ax-icn 10333 ax-addcl 10334 ax-addrcl 10335 ax-mulcl 10336 ax-mulrcl 10337 ax-mulcom 10338 ax-addass 10339 ax-mulass 10340 ax-distr 10341 ax-i2m1 10342 ax-1ne0 10343 ax-1rid 10344 ax-rnegex 10345 ax-rrecex 10346 ax-cnre 10347 ax-pre-lttri 10348 ax-pre-lttrn 10349 ax-pre-ltadd 10350 ax-pre-mulgt0 10351 ax-pre-sup 10352

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-fal 1615 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rmo 3098 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4674 df-int 4713 df-iun 4757 df-br 4889 df-opab 4951 df-mpt 4968 df-tr 4990 df-id 5263 df-eprel 5268 df-po 5276 df-so 5277 df-fr 5316 df-se 5317 df-we 5318 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-pred 5935 df-ord 5981 df-on 5982 df-lim 5983 df-suc 5984 df-iota 6101 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-fv 6145 df-isom 6146 df-riota 6885 df-ov 6927 df-oprab 6928 df-mpt2 6929 df-om 7346 df-1st 7447 df-2nd 7448 df-wrecs 7691 df-recs 7753 df-rdg 7791 df-1o 7845 df-oadd 7849 df-er 8028 df-map 8144 df-en 8244 df-dom 8245 df-sdom 8246 df-fin 8247 df-sup 8638 df-oi 8706 df-card 9100 df-pnf 10415 df-mnf 10416 df-xr 10417 df-ltxr 10418 df-le 10419 df-sub 10610 df-neg 10611 df-div 11036 df-nn 11380 df-2 11443 df-3 11444 df-n0 11648 df-z 11734 df-uz 11998 df-rp 12143 df-ico 12498 df-fz 12649 df-fzo 12790 df-seq 13125 df-exp 13184 df-hash 13442 df-cj 14252 df-re 14253 df-im 14254 df-sqrt 14388 df-abs 14389 df-clim 14636 df-sum 14834

This theorem is referenced by: dvnprodlem2 41104

W3C validator