Theorem dvnprodlem1 46587

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

Hypotheses

Ref	Expression
dvnprodlem1.c	⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
dvnprodlem1.j	⊢ (𝜑 → 𝐽 ∈ ℕ0)
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 2770	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
2		0zd 12603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3		dvnprodlem1.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℕ0)
4	3	nn0zd 12616	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℤ)
5	4	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6		oveq2 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
7	6	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝐽 → ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
8		eqeq2 2781	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
9	7, 8	rabeqbidv 3440	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
10		dvnprodlem1.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
11		oveq2 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})))
12		sumeq1 15740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡))
13	12	eqeq1d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛))
14	11, 13	rabeqbidv 3440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛})
15	14	mpteq2dv 5207	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
16		dvnprodlem1.t	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ Fin)
17		dvnprodlem1.rzt	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
18	16, 17	sselpwd 5299	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
19		nn0ex 12510	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 ∈ V
20	19	mptex 7222	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V
21	20	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}) ∈ V)
22	10, 15, 18, 21	fvmptd3 7014	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝑛}))
23		ovex 7444	. . . . . . . . . . . . . . . . 17 ⊢ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ V
24	23	rabex 5310	. . . . . . . . . . . . . . . 16 ⊢ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V
25	24	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ∈ V)
26	9, 22, 3, 25	fvmptd4 7015	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
27		ssrab2 4040	. . . . . . . . . . . . . 14 ⊢ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))
28	26, 27	eqsstrdi 3987	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
29	28	sselda 3943	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
30		elmapi 8846	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
31	29, 30	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
32		dvnprodlem1.z	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ 𝑇)
33		snidg 4629	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ 𝑇 → 𝑍 ∈ {𝑍})
34		elun2 4142	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
35	32, 33, 34	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ∈ (𝑅 ∪ {𝑍}))
36	35	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
37	31, 36	ffvelcdmd 7081	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ (0...𝐽))
38	37	elfzelzd 13553	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℤ)
39	5, 38	zsubcld 12705	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
40		elfzle2 13556	. . . . . . . . . 10 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → (𝑐‘𝑍) ≤ 𝐽)
41	37, 40	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ≤ 𝐽)
42	5	zred 12700	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
43	38	zred 12700	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℝ)
44	42, 43	subge0d 11804	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐‘𝑍)) ↔ (𝑐‘𝑍) ≤ 𝐽))
45	41, 44	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐‘𝑍)))
46		elfzle1 13555	. . . . . . . . . 10 ⊢ ((𝑐‘𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑍))
47	37, 46	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐‘𝑍))
48	42, 43	subge02d 11806	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐‘𝑍) ↔ (𝐽 − (𝑐‘𝑍)) ≤ 𝐽))
49	47, 48	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ≤ 𝐽)
50	2, 5, 39, 45, 49	elfzd 13543	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽))
51		eqidd 2770	. . . . . . . . . . 11 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → 𝑅 = 𝑅)
52		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → 𝑒 = (𝑐 ↾ 𝑅))
53	52	fveq1d 6884	. . . . . . . . . . 11 ⊢ ((𝑒 = (𝑐 ↾ 𝑅) ∧ 𝑡 ∈ 𝑅) → (𝑒‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
54	51, 53	sumeq12rdv 15758	. . . . . . . . . 10 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡))
55	54	eqeq1d 2771	. . . . . . . . 9 ⊢ (𝑒 = (𝑐 ↾ 𝑅) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍)) ↔ Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍))))
56		ovexd 7446	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐‘𝑍))) ∈ V)
57	17	unssad 4152	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ⊆ 𝑇)
58	16, 57	ssfid 9229	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Fin)
59	58	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
60		elmapfn 8862	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
61	29, 60	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
62		ssun1 4137	. . . . . . . . . . . . 13 ⊢ 𝑅 ⊆ (𝑅 ∪ {𝑍})
63	62	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
64	61, 63	fnssresd 6660	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) Fn 𝑅)
65		nfv 1941	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡𝜑
66		nfcv 2931	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝒫 𝑇
67		nfcv 2931	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡ℕ0
68		nfcv 2931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑡𝑠
69	68	nfsum1 15741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡)
70	69	nfeq1 2946	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛
71		nfcv 2931	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡((0...𝑛) ↑m 𝑠)
72	70, 71	nfrabw 3458	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}
73	67, 72	nfmpt 5211	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})
74	66, 73	nfmpt 5211	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))
75	10, 74	nfcxfr 2929	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡𝐶
76		nfcv 2931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝑅 ∪ {𝑍})
77	75, 76	nffv 6892	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡(𝐶‘(𝑅 ∪ {𝑍}))
78		nfcv 2931	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝐽
79	77, 78	nffv 6892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
80	79	nfcri 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
81	65, 80	nfan 1926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
82		fvres 6901	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
83	82	adantl 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
84		0zd 12603	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ∈ ℤ)
85	39	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝐽 − (𝑐‘𝑍)) ∈ ℤ)
86	31	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
87	63	sselda 3943	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
88	86, 87	ffvelcdmd 7081	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...𝐽))
89	88	elfzelzd 13553	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ ℤ)
90		elfzle1 13555	. . . . . . . . . . . . . . 15 ⊢ ((𝑐‘𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑡))
91	88, 90	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 0 ≤ (𝑐‘𝑡))
92	58	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑅 ∈ Fin)
93		fzssre 45960	. . . . . . . . . . . . . . . . . 18 ⊢ (0...𝐽) ⊆ ℝ
94	31	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
95	63	sselda 3943	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
96	94, 95	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ (0...𝐽))
97	93, 96	sselid 3941	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
98	97	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℝ)
99		elfzle1 13555	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐‘𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐‘𝑟))
100	96, 99	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
101	100	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) ∧ 𝑟 ∈ 𝑅) → 0 ≤ (𝑐‘𝑟))
102		fveq2 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → (𝑐‘𝑟) = (𝑐‘𝑡))
103		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → 𝑡 ∈ 𝑅)
104	92, 98, 101, 102, 103	fsumge1 15849	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
105	97	recnd 11237	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟 ∈ 𝑅) → (𝑐‘𝑟) ∈ ℂ)
106	59, 105	fsumcl 15784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) ∈ ℂ)
107	38	zcnd 12701	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) ∈ ℂ)
108	102	cbvsumv 15747	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡)
109		nfv 1941	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟(𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
110		nfcv 2931	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟(𝑐‘𝑍)
111	32	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ 𝑇)
112		dvnprodlem1.zr	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑅)
113	112	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍 ∈ 𝑅)
114		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑍 → (𝑐‘𝑟) = (𝑐‘𝑍))
115	109, 110, 59, 111, 113, 105, 114, 107	fsumsplitsn 15795	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑟) = (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)))
116		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
117	26	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
118	116, 117	eleqtrd 2871	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
119		rabid 3443	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
120	118, 119	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽))
121	120	simprd 500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽)
122	108, 115, 121	3eqtr3a 2828	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) + (𝑐‘𝑍)) = 𝐽)
123	106, 107, 122	mvlraddd 11624	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
124	123	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = (𝐽 − (𝑐‘𝑍)))
125	104, 124	breqtrd 5139	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ≤ (𝐽 − (𝑐‘𝑍)))
126	84, 85, 89, 91, 125	elfzd 13543	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
127	83, 126	eqeltrd 2869	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
128	81, 127	ralrimia 3270	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍))))
129		ffnfv 7115	. . . . . . . . . . 11 ⊢ ((𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))) ↔ ((𝑐 ↾ 𝑅) Fn 𝑅 ∧ ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐‘𝑍)))))
130	64, 128, 129	sylanbrc 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅):𝑅⟶(0...(𝐽 − (𝑐‘𝑍))))
131	56, 59, 130	elmapdd 8838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅))
132	82	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡 ∈ 𝑅 → ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡)))
133	81, 132	ralrimi 3269	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝑐‘𝑡))
134	133	sumeq2d 15752	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
135	102	cbvsumv 15747	. . . . . . . . . . . 12 ⊢ Σ𝑟 ∈ 𝑅 (𝑐‘𝑟) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡)
136	135	eqcomi 2778	. . . . . . . . . . 11 ⊢ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟)
137	136	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑟 ∈ 𝑅 (𝑐‘𝑟))
138	134, 137, 123	3eqtrd 2808	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ 𝑅 ((𝑐 ↾ 𝑅)‘𝑡) = (𝐽 − (𝑐‘𝑍)))
139	55, 131, 138	elrabd 3659	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
140		fveq1 6881	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑡) = (𝑒‘𝑡))
141	140	sumeq2sdv 15754	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑒 → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑒‘𝑡))
142	141	eqeq1d 2771	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑒 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚))
143	142	cbvrabv 3432	. . . . . . . . . . 11 ⊢ {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚}
144	143	a1i 11	. . . . . . . . . 10 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
145		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐‘𝑍))))
146	145	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → ((0...𝑚) ↑m 𝑅) = ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅))
147	146	rabeqdv 3437	. . . . . . . . . 10 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚})
148		eqeq2 2781	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → (Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚 ↔ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))))
149	148	rabbidv 3429	. . . . . . . . . 10 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
150	144, 147, 149	3eqtrd 2808	. . . . . . . . 9 ⊢ (𝑚 = (𝐽 − (𝑐‘𝑍)) → {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
151		oveq2 7419	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑅 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅))
152		sumeq1 15740	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑅 → Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 (𝑐‘𝑡))
153	152	eqeq1d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑅 → (Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛))
154	151, 153	rabeqbidv 3440	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛})
155	154	mpteq2dv 5207	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
156	16, 57	sselpwd 5299	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ 𝒫 𝑇)
157	19	mptex 7222	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V
158	157	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) ∈ V)
159	10, 155, 156, 158	fvmptd3 7014	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
160	159	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
161		oveq2 7419	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
162	161	oveq1d 7426	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑚 → ((0...𝑛) ↑m 𝑅) = ((0...𝑚) ↑m 𝑅))
163		eqeq2 2781	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑚 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚))
164	162, 163	rabeqbidv 3440	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
165	164	cbvmptv 5217	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚})
166	160, 165	eqtrdi 2820	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶‘𝑅) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑚}))
167		elnn0z 12604	. . . . . . . . . 10 ⊢ ((𝐽 − (𝑐‘𝑍)) ∈ ℕ0 ↔ ((𝐽 − (𝑐‘𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐‘𝑍))))
168	39, 45, 167	sylanbrc 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ ℕ0)
169		ovex 7444	. . . . . . . . . . 11 ⊢ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∈ V
170	169	rabex 5310	. . . . . . . . . 10 ⊢ {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V
171	170	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))} ∈ V)
172	150, 166, 168, 171	fvmptd4 7015	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐‘𝑍))) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑒‘𝑡) = (𝐽 − (𝑐‘𝑍))})
173	139, 172	eleqtrrd 2872	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
174	50, 173	jca 520	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
175		ovexd 7446	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) ∈ V)
176		vex 3465	. . . . . . . 8 ⊢ 𝑐 ∈ V
177	176	resex 6029	. . . . . . 7 ⊢ (𝑐 ↾ 𝑅) ∈ V
178		opeq12 4842	. . . . . . . . . 10 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
179	178	eqeq2d 2780	. . . . . . . . 9 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
180		eleq1 2857	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
181	180	adantr 485	. . . . . . . . . 10 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽)))
182		simpr 489	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → 𝑑 = (𝑐 ↾ 𝑅))
183		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐽 − (𝑐‘𝑍)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
184	183	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝐶‘𝑅)‘𝑘) = ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))
185	182, 184	eleq12d 2863	. . . . . . . . . 10 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → (𝑑 ∈ ((𝐶‘𝑅)‘𝑘) ↔ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))
186	181, 185	anbi12d 643	. . . . . . . . 9 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))))
187	179, 186	anbi12d 643	. . . . . . . 8 ⊢ ((𝑘 = (𝐽 − (𝑐‘𝑍)) ∧ 𝑑 = (𝑐 ↾ 𝑅)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍)))))))
188	187	spc2egv 3565	. . . . . . 7 ⊢ (((𝐽 − (𝑐‘𝑍)) ∈ V ∧ (𝑐 ↾ 𝑅) ∈ V) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
189	175, 177, 188	sylancl 597	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∧ ((𝐽 − (𝑐‘𝑍)) ∈ (0...𝐽) ∧ (𝑐 ↾ 𝑅) ∈ ((𝐶‘𝑅)‘(𝐽 − (𝑐‘𝑍))))) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘)))))
190	1, 174, 189	mp2and 711	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
191		eliunxp 5824	. . . . 5 ⊢ (⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘∃𝑑(⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶‘𝑅)‘𝑘))))
192	190, 191	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
193		dvnprodlem1.d	. . . 4 ⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
194	192, 193	fmptd 7110	. . 3 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
195	79	nfcri 2923	. . . . . . . . . 10 ⊢ Ⅎ𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
196	80, 195	nfan 1926	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
197	65, 196	nfan 1926	. . . . . . . 8 ⊢ Ⅎ𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
198		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑡(𝐷‘𝑐) = (𝐷‘𝑒)
199	197, 198	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒))
200	83	eqcomd 2775	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
201	200	adantlrr 733	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
202	201	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡))
203	193	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
204		opex 5446	. . . . . . . . . . . . . . . . 17 ⊢ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V
205	204	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ ∈ V)
206	203, 205	fvmpt2d 7004	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)
207	206	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2nd ‘(𝐷‘𝑐)) = (2nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
208	207	fveq1d 6884	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘(𝐷‘𝑐))‘𝑡) = ((2nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡))
209		ovex 7444	. . . . . . . . . . . . . . 15 ⊢ (𝐽 − (𝑐‘𝑍)) ∈ V
210	209, 177	op2nd 7995	. . . . . . . . . . . . . 14 ⊢ (2nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝑐 ↾ 𝑅)
211	210	fveq1i 6883	. . . . . . . . . . . . 13 ⊢ ((2nd ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)‘𝑡) = ((𝑐 ↾ 𝑅)‘𝑡)
212	208, 211	eqtr2di 2821	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2nd ‘(𝐷‘𝑐))‘𝑡))
213	212	adantrr 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2nd ‘(𝐷‘𝑐))‘𝑡))
214	213	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑐 ↾ 𝑅)‘𝑡) = ((2nd ‘(𝐷‘𝑐))‘𝑡))
215		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = (𝐷‘𝑒))
216		fveq1 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑒 → (𝑐‘𝑍) = (𝑒‘𝑍))
217	216	oveq2d 7427	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑒 → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝑒‘𝑍)))
218		reseq1 5973	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑒 → (𝑐 ↾ 𝑅) = (𝑒 ↾ 𝑅))
219	217, 218	opeq12d 4848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
220		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
221		opex 5446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V
222	221	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩ ∈ V)
223	193, 219, 220, 222	fvmptd3 7014	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
224	223	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑒) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
225	215, 224	eqtrd 2804	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐷‘𝑐) = ⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩)
226	225	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2nd ‘(𝐷‘𝑐)) = (2nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
227	226	adantlrl 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (2nd ‘(𝐷‘𝑐)) = (2nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
228	227	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2nd ‘(𝐷‘𝑐)) = (2nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
229		ovex 7444	. . . . . . . . . . . . . 14 ⊢ (𝐽 − (𝑒‘𝑍)) ∈ V
230		vex 3465	. . . . . . . . . . . . . . 15 ⊢ 𝑒 ∈ V
231	230	resex 6029	. . . . . . . . . . . . . 14 ⊢ (𝑒 ↾ 𝑅) ∈ V
232	229, 231	op2nd 7995	. . . . . . . . . . . . 13 ⊢ (2nd ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝑒 ↾ 𝑅)
233	228, 232	eqtrdi 2820	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (2nd ‘(𝐷‘𝑐)) = (𝑒 ↾ 𝑅))
234	233	fveq1d 6884	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘(𝐷‘𝑐))‘𝑡) = ((𝑒 ↾ 𝑅)‘𝑡))
235		fvres 6901	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑅 → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
236	235	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((𝑒 ↾ 𝑅)‘𝑡) = (𝑒‘𝑡))
237	234, 236	eqtrd 2804	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘(𝐷‘𝑐))‘𝑡) = (𝑒‘𝑡))
238	202, 214, 237	3eqtrd 2808	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
239	238	adantlr 727	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
240		elunnel1 4114	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 ∈ {𝑍})
241		elsni 4609	. . . . . . . . . . 11 ⊢ (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
242	240, 241	syl 18	. . . . . . . . . 10 ⊢ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
243	242	adantll 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
244		simpr 489	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
245	244	fveq2d 6886	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑐‘𝑍))
246	3	nn0cnd 12567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐽 ∈ ℂ)
247	246	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
248	247, 107	nncand 11574	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝑐‘𝑍))
249	248	eqcomd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
250	249	adantrr 729	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
251	250	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝐽 − (𝐽 − (𝑐‘𝑍))))
252	206	fveq2d 6886	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷‘𝑐)) = (1st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩))
253	209, 177	op1st 7994	. . . . . . . . . . . . . . . . 17 ⊢ (1st ‘⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩) = (𝐽 − (𝑐‘𝑍))
254	252, 253	eqtr2di 2821	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐‘𝑍)) = (1st ‘(𝐷‘𝑐)))
255	254	oveq2d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1st ‘(𝐷‘𝑐))))
256	255	adantrr 729	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1st ‘(𝐷‘𝑐))))
257	256	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑐‘𝑍))) = (𝐽 − (1st ‘(𝐷‘𝑐))))
258		fveq2 6882	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷‘𝑐) = (𝐷‘𝑒) → (1st ‘(𝐷‘𝑐)) = (1st ‘(𝐷‘𝑒)))
259	258	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1st ‘(𝐷‘𝑐)) = (1st ‘(𝐷‘𝑒)))
260	223	fveq2d 6886	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷‘𝑒)) = (1st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
261	260	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1st ‘(𝐷‘𝑒)) = (1st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩))
262	229, 231	op1st 7994	. . . . . . . . . . . . . . . . . 18 ⊢ (1st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍))
263	262	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1st ‘⟨(𝐽 − (𝑒‘𝑍)), (𝑒 ↾ 𝑅)⟩) = (𝐽 − (𝑒‘𝑍)))
264	259, 261, 263	3eqtrd 2808	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (1st ‘(𝐷‘𝑐)) = (𝐽 − (𝑒‘𝑍)))
265	264	oveq2d 7427	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1st ‘(𝐷‘𝑐))) = (𝐽 − (𝐽 − (𝑒‘𝑍))))
266	246	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
267		fzsscn 45957	. . . . . . . . . . . . . . . . . 18 ⊢ (0...𝐽) ⊆ ℂ
268		eleq1w 2852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
269	268	anbi2d 641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑒 → ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
270		feq1 6684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
271	269, 270	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑒 → (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
272	271, 31	chvarvv 2016	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
273	35	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
274	272, 273	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ (0...𝐽))
275	267, 274	sselid 3941	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒‘𝑍) ∈ ℂ)
276	266, 275	nncand 11574	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
277	276	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (𝐽 − (𝑒‘𝑍))) = (𝑒‘𝑍))
278	265, 277	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
279	278	adantlrl 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝐽 − (1st ‘(𝐷‘𝑐))) = (𝑒‘𝑍))
280	251, 257, 279	3eqtrd 2808	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐‘𝑍) = (𝑒‘𝑍))
281	280	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑍) = (𝑒‘𝑍))
282		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑡) = (𝑒‘𝑍))
283	282	eqcomd 2775	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑍 → (𝑒‘𝑍) = (𝑒‘𝑡))
284	283	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑒‘𝑍) = (𝑒‘𝑡))
285	245, 281, 284	3eqtrd 2808	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
286	285	adantlr 727	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐‘𝑡) = (𝑒‘𝑡))
287	243, 286	syldan 602	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = (𝑒‘𝑡))
288	239, 287	pm2.61dan 824	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐‘𝑡) = (𝑒‘𝑡))
289	199, 288	ralrimia 3270	. . . . . 6 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡))
290	61	adantrr 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
291	290	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
292	272	ffnd 6707	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
293	292	adantrl 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
294	293	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
295		eqfnfv 7026	. . . . . . 7 ⊢ ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
296	291, 294, 295	syl2anc 595	. . . . . 6 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = (𝑒‘𝑡)))
297	289, 296	mpbird 260	. . . . 5 ⊢ (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷‘𝑐) = (𝐷‘𝑒)) → 𝑐 = 𝑒)
298	297	ex 417	. . . 4 ⊢ ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
299	298	ralrimivva 3214	. . 3 ⊢ (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒))
300		dff13 7253	. . 3 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷‘𝑐) = (𝐷‘𝑒) → 𝑐 = 𝑒)))
301	194, 299, 300	sylanbrc 594	. 2 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
302		eliun 4962	. . . . . . . . 9 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
303	302	biimpi 219	. . . . . . . 8 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
304	303	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
305		nfv 1941	. . . . . . . . 9 ⊢ Ⅎ𝑘𝜑
306		nfiu1 4994	. . . . . . . . . 10 ⊢ Ⅎ𝑘∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
307	306	nfcri 2923	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))
308	305, 307	nfan 1926	. . . . . . . 8 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
309		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}
310		eleq1w 2852	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑟 → (𝑡 ∈ 𝑅 ↔ 𝑟 ∈ 𝑅))
311		fveq2 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑟 → ((2nd ‘𝑝)‘𝑡) = ((2nd ‘𝑝)‘𝑟))
312	310, 311	ifbieq1d 4515	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑟 → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))
313	312	cbvmptv 5217	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))
314	313	eqeq2i 2782	. . . . . . . . . . . . 13 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝)))))
315		fveq1 6881	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝)))) → (𝑐‘𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))‘𝑡))
316	315	sumeq2sdv 15754	. . . . . . . . . . . . 13 ⊢ (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))‘𝑡))
317	314, 316	sylbi 220	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))‘𝑡))
318	317	eqeq1d 2771	. . . . . . . . . . 11 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))‘𝑡) = 𝐽))
319		ovexd 7446	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (0...𝐽) ∈ V)
320	16, 17	ssexd 5295	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
321	320	3ad2ant1 1149	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
322		nfv 1941	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡 𝑘 ∈ (0...𝐽)
323		nfcv 2931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡{𝑘}
324		nfcv 2931	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑅
325	75, 324	nffv 6892	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝐶‘𝑅)
326		nfcv 2931	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑘
327	325, 326	nffv 6892	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡((𝐶‘𝑅)‘𝑘)
328	323, 327	nfxp 5695	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡({𝑘} × ((𝐶‘𝑅)‘𝑘))
329	328	nfcri 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))
330	65, 322, 329	nf3an 1928	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)))
331		0zd 12603	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
332	4	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
333	332	3ad2antl1 1202	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
334		iftrue 4496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ 𝑅 → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = ((2nd ‘𝑝)‘𝑡))
335	334	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = ((2nd ‘𝑝)‘𝑡))
336		xp2nd 8019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (2nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
337	336	3ad2ant3 1151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2nd ‘𝑝) ∈ ((𝐶‘𝑅)‘𝑘))
338		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
339	338	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → ((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅))
340		eqeq2 2781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛 ↔ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘))
341	339, 340	rabeqbidv 3440	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
342	159	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐶‘𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑛}))
343		elfznn0 13648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
344	343	adantl 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
345		ovex 7444	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0...𝑘) ↑m 𝑅) ∈ V
346	345	rabex 5310	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V
347	346	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ∈ V)
348	341, 342, 344, 347	fvmptd4 7015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
349	348	3adant3 1148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((𝐶‘𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
350	337, 349	eleqtrd 2871	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘})
351		elrabi 3653	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} → (2nd ‘𝑝) ∈ ((0...𝑘) ↑m 𝑅))
352		elmapi 8846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2nd ‘𝑝) ∈ ((0...𝑘) ↑m 𝑅) → (2nd ‘𝑝):𝑅⟶(0...𝑘))
353	350, 351, 352	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2nd ‘𝑝):𝑅⟶(0...𝑘))
354	353	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2nd ‘𝑝):𝑅⟶(0...𝑘))
355	354	ffvelcdmda 7080	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
356	355	elfzelzd 13553	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘𝑝)‘𝑡) ∈ ℤ)
357	335, 356	eqeltrd 2869	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ∈ ℤ)
358	242	adantll 726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 𝑡 = 𝑍)
359		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
360	112	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
361	359, 360	eqneltrd 2889	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
362	361	iffalsed 4501	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = (𝐽 − (1st ‘𝑝)))
363	362	3ad2antl1 1202	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = (𝐽 − (1st ‘𝑝)))
364	4	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
365	364	3ad2antl1 1202	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
366		xp1st 8018	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1st ‘𝑝) ∈ {𝑘})
367		elsni 4609	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1st ‘𝑝) ∈ {𝑘} → (1st ‘𝑝) = 𝑘)
368	366, 367	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1st ‘𝑝) = 𝑘)
369	368	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1st ‘𝑝) = 𝑘)
370		elfzelz 13552	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
371	370	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
372	369, 371	eqeltrd 2869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1st ‘𝑝) ∈ ℤ)
373	372	3adant1 1146	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1st ‘𝑝) ∈ ℤ)
374	373	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1st ‘𝑝) ∈ ℤ)
375	365, 374	zsubcld 12705	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st ‘𝑝)) ∈ ℤ)
376	363, 375	eqeltrd 2869	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ∈ ℤ)
377	376	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ∈ ℤ)
378	358, 377	syldan 602	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ∈ ℤ)
379	357, 378	pm2.61dan 824	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ∈ ℤ)
380	353	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘))
381		elfzle1 13555	. . . . . . . . . . . . . . . . . 18 ⊢ (((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2nd ‘𝑝)‘𝑡))
382	380, 381	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ ((2nd ‘𝑝)‘𝑡))
383	334	eqcomd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝑅 → ((2nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
384	383	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘𝑝)‘𝑡) = if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
385	382, 384	breqtrd 5139	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
386	385	adantlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
387		simpll 778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → (𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))))
388		elfzle2 13556	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ≤ 𝐽)
389		elfzel2 13550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
390	389	zred 12700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
391	93	sseli 3939	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
392	390, 391	subge0d 11804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽 − 𝑘) ↔ 𝑘 ≤ 𝐽))
393	388, 392	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽 − 𝑘))
394	393	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
395	394	3ad2antl2 1203	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽 − 𝑘))
396	361	3ad2antl1 1202	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡 ∈ 𝑅)
397	396	iffalsed 4501	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = (𝐽 − (1st ‘𝑝)))
398	368	3ad2ant3 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1st ‘𝑝) = 𝑘)
399	398	oveq2d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1st ‘𝑝)) = (𝐽 − 𝑘))
400	399	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st ‘𝑝)) = (𝐽 − 𝑘))
401	397, 400	eqtr2d 2805	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) = if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
402	395, 401	breqtrd 5139	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
403	387, 358, 402	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → 0 ≤ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
404	386, 403	pm2.61dan 824	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
405		simpl2 1209	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → 𝑘 ∈ (0...𝐽))
406		elfzelz 13552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd ‘𝑝)‘𝑡) ∈ ℤ)
407	406	zred 12700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd ‘𝑝)‘𝑡) ∈ ℝ)
408	407	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd ‘𝑝)‘𝑡) ∈ ℝ)
409	391	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
410	390	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
411		elfzle2 13556	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd ‘𝑝)‘𝑡) ≤ 𝑘)
412	411	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd ‘𝑝)‘𝑡) ≤ 𝑘)
413	388	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ≤ 𝐽)
414	408, 409, 410, 412, 413	letrd 11367	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2nd ‘𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd ‘𝑝)‘𝑡) ≤ 𝐽)
415	380, 405, 414	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘𝑝)‘𝑡) ≤ 𝐽)
416	415	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘𝑝)‘𝑡) ≤ 𝐽)
417	335, 416	eqbrtrd 5135	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ≤ 𝐽)
418	344	nn0ge0d 12568	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
419	390	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
420	391	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
421	419, 420	subge02d 11806	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽 − 𝑘) ≤ 𝐽))
422	418, 421	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (𝐽 − 𝑘) ≤ 𝐽)
423	422	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
424	423	3adantl3 1185	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − 𝑘) ≤ 𝐽)
425	401, 424	eqbrtrrd 5137	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ≤ 𝐽)
426	387, 358, 425	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ≤ 𝐽)
427	417, 426	pm2.61dan 824	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ≤ 𝐽)
428	331, 333, 379, 404, 427	elfzd 13543	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ∈ (0...𝐽))
429	330, 428	fmptd2f 45877	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
430	319, 321, 429	elmapdd 8838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
431		eleq1w 2852	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → (𝑟 ∈ 𝑅 ↔ 𝑡 ∈ 𝑅))
432		fveq2 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → ((2nd ‘𝑝)‘𝑟) = ((2nd ‘𝑝)‘𝑡))
433	431, 432	ifbieq1d 4515	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑡 → if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))) = if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
434		eqidd 2770	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝)))))
435		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
436	433, 434, 435, 379	fvmptd4 7015	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
437	330, 436	ralrimia 3270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))‘𝑡) = if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
438	437	sumeq2d 15752	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))
439		nfcv 2931	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝)))
440	58	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑅 ∈ Fin)
441	32	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑍 ∈ 𝑇)
442	112	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ¬ 𝑍 ∈ 𝑅)
443	334	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = ((2nd ‘𝑝)‘𝑡))
444	380	elfzelzd 13553	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘𝑝)‘𝑡) ∈ ℤ)
445	444	zcnd 12701	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → ((2nd ‘𝑝)‘𝑡) ∈ ℂ)
446	443, 445	eqeltrd 2869	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑡 ∈ 𝑅) → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) ∈ ℂ)
447		eleq1 2857	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑍 → (𝑡 ∈ 𝑅 ↔ 𝑍 ∈ 𝑅))
448		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑍 → ((2nd ‘𝑝)‘𝑡) = ((2nd ‘𝑝)‘𝑍))
449	447, 448	ifbieq1d 4515	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑍 → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝))))
450	112	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ¬ 𝑍 ∈ 𝑅)
451	450	iffalsed 4501	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝))) = (𝐽 − (1st ‘𝑝)))
452	451	3adant2 1147	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝))) = (𝐽 − (1st ‘𝑝)))
453	4	3ad2ant1 1149	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
454	453, 373	zsubcld 12705	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1st ‘𝑝)) ∈ ℤ)
455	454	zcnd 12701	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐽 − (1st ‘𝑝)) ∈ ℂ)
456	452, 455	eqeltrd 2869	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝))) ∈ ℂ)
457	330, 439, 440, 441, 442, 446, 449, 456	fsumsplitsn 15795	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝)))))
458	334	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 → if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = ((2nd ‘𝑝)‘𝑡)))
459	330, 458	ralrimi 3269	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∀𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = ((2nd ‘𝑝)‘𝑡))
460	459	sumeq2d 15752	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = Σ𝑡 ∈ 𝑅 ((2nd ‘𝑝)‘𝑡))
461		eqidd 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (2nd ‘𝑝) → 𝑅 = 𝑅)
462		simpl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (2nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → 𝑐 = (2nd ‘𝑝))
463	462	fveq1d 6884	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = (2nd ‘𝑝) ∧ 𝑡 ∈ 𝑅) → (𝑐‘𝑡) = ((2nd ‘𝑝)‘𝑡))
464	461, 463	sumeq12rdv 15758	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (2nd ‘𝑝) → Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = Σ𝑡 ∈ 𝑅 ((2nd ‘𝑝)‘𝑡))
465	464	eqeq1d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (2nd ‘𝑝) → (Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘 ↔ Σ𝑡 ∈ 𝑅 ((2nd ‘𝑝)‘𝑡) = 𝑘))
466	465	elrab 3657	. . . . . . . . . . . . . . . . 17 ⊢ ((2nd ‘𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡 ∈ 𝑅 (𝑐‘𝑡) = 𝑘} ↔ ((2nd ‘𝑝) ∈ ((0...𝑘) ↑m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((2nd ‘𝑝)‘𝑡) = 𝑘))
467	350, 466	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ((2nd ‘𝑝) ∈ ((0...𝑘) ↑m 𝑅) ∧ Σ𝑡 ∈ 𝑅 ((2nd ‘𝑝)‘𝑡) = 𝑘))
468	467	simprd 500	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 ((2nd ‘𝑝)‘𝑡) = 𝑘)
469	460, 468	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) = 𝑘)
470	442	iffalsed 4501	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝))) = (𝐽 − (1st ‘𝑝)))
471	470, 399	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝))) = (𝐽 − 𝑘))
472	469, 471	oveq12d 7429	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝)))) = (𝑘 + (𝐽 − 𝑘)))
473	267	sseli 3939	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
474	473	3ad2ant2 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
475	246	3ad2ant1 1149	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
476	474, 475	pncan3d 11572	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 + (𝐽 − 𝑘)) = 𝐽)
477	472, 476	eqtrd 2804	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (Σ𝑡 ∈ 𝑅 if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))) + if(𝑍 ∈ 𝑅, ((2nd ‘𝑝)‘𝑍), (𝐽 − (1st ‘𝑝)))) = 𝐽)
478	438, 457, 477	3eqtrd 2808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))))‘𝑡) = 𝐽)
479	318, 430, 478	elrabd 3659	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
480	479	3exp 1135	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
481	480	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})))
482	308, 309, 481	rexlimd 3278	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽}))
483	304, 482	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽})
484	26	eqcomd 2775	. . . . . . 7 ⊢ (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
485	484	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐‘𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
486	483, 485	eleqtrd 2871	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
487		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))))
488	487, 313	eqtrdi 2820	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝)))))
489		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → 𝑟 = 𝑍)
490	112	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑍 ∈ 𝑅)
491	489, 490	eqneltrd 2889	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → ¬ 𝑟 ∈ 𝑅)
492	491	iffalsed 4501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))) = (𝐽 − (1st ‘𝑝)))
493	492	adantlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟 ∈ 𝑅, ((2nd ‘𝑝)‘𝑟), (𝐽 − (1st ‘𝑝))) = (𝐽 − (1st ‘𝑝)))
494	35	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
495		ovexd 7446	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝐽 − (1st ‘𝑝)) ∈ V)
496	488, 493, 494, 495	fvmptd 6998	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝑐‘𝑍) = (𝐽 − (1st ‘𝑝)))
497	496	oveq2d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1st ‘𝑝))))
498	497	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (𝐽 − (𝐽 − (1st ‘𝑝))))
499	246	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → 𝐽 ∈ ℂ)
500		nfv 1941	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(1st ‘𝑝) ∈ (0...𝐽)
501		simpl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
502	369, 501	eqeltrd 2869	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (1st ‘𝑝) ∈ (0...𝐽))
503	502	ex 417	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1st ‘𝑝) ∈ (0...𝐽)))
504	503	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1st ‘𝑝) ∈ (0...𝐽))))
505	307, 500, 504	rexlimd 3278	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1st ‘𝑝) ∈ (0...𝐽)))
506	303, 505	mpd 16	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1st ‘𝑝) ∈ (0...𝐽))
507	506	elfzelzd 13553	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1st ‘𝑝) ∈ ℤ)
508	507	zcnd 12701	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (1st ‘𝑝) ∈ ℂ)
509	508	ad2antlr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (1st ‘𝑝) ∈ ℂ)
510	499, 509	nncand 11574	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝐽 − (𝐽 − (1st ‘𝑝))) = (1st ‘𝑝))
511	498, 510	eqtrd 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝐽 − (𝑐‘𝑍)) = (1st ‘𝑝))
512		reseq1 5973	. . . . . . . . . 10 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) → (𝑐 ↾ 𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ↾ 𝑅))
513	512	adantl 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝑐 ↾ 𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ↾ 𝑅))
514	62	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
515	514	resmptd 6043	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ↾ 𝑅) = (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))))
516		nfv 1941	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (2nd ‘𝑝)
517	334	mpteq2ia 5208	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (𝑡 ∈ 𝑅 ↦ ((2nd ‘𝑝)‘𝑡))
518	353	feqmptd 6950	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (2nd ‘𝑝) = (𝑡 ∈ 𝑅 ↦ ((2nd ‘𝑝)‘𝑡)))
519	517, 518	eqtr4id 2823	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (2nd ‘𝑝))
520	519	3exp 1135	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (2nd ‘𝑝))))
521	520	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (2nd ‘𝑝))))
522	308, 516, 521	rexlimd 3278	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (2nd ‘𝑝)))
523	304, 522	mpd 16	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (2nd ‘𝑝))
524	523	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝑡 ∈ 𝑅 ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) = (2nd ‘𝑝))
525	513, 515, 524	3eqtrd 2808	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → (𝑐 ↾ 𝑅) = (2nd ‘𝑝))
526	511, 525	opeq12d 4848	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) → ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩ = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩)
527		opex 5446	. . . . . . . 8 ⊢ ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ V
528	527	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ V)
529	193, 526, 486, 528	fvmptd2 6999	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))) = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩)
530		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑘⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ = 𝑝
531		1st2nd2 8025	. . . . . . . . . 10 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩)
532	531	eqcomd 2775	. . . . . . . . 9 ⊢ (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ = 𝑝)
533	532	2a1i 12	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ = 𝑝)))
534	308, 530, 533	rexlimd 3278	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶‘𝑅)‘𝑘)) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ = 𝑝))
535	304, 534	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ = 𝑝)
536	529, 535	eqtr2d 2805	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))))
537		fveq2 6882	. . . . . 6 ⊢ (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) → (𝐷‘𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝))))))
538	537	rspceeqv 3611	. . . . 5 ⊢ (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡 ∈ 𝑅, ((2nd ‘𝑝)‘𝑡), (𝐽 − (1st ‘𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
539	486, 536, 538	syl2anc 595	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
540	539	ralrimiva 3163	. . 3 ⊢ (𝜑 → ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐))
541		dffo3 7098	. . 3 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ ∀𝑝 ∈ ∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷‘𝑐)))
542	194, 540, 541	sylanbrc 594	. 2 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
543		df-f1o 6544	. 2 ⊢ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))))
544	301, 542, 543	sylanbrc 594	1 ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  {crab 3422  Vcvv 3461   ∪ cun 3909   ⊆ wss 3911  ifcif 4490  𝒫 cpw 4565  {csn 4592  ⟨cop 4598  ∪ ciun 4958   class class class wbr 5111   ↦ cmpt 5194   × cxp 5660   ↾ cres 5664   Fn wfn 6532  ⟶wf 6533  –1-1→wf1 6534  –onto→wfo 6535  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7411  1^st c1st 7984  2^nd c2nd 7985   ↑_m cmap 8824  Fincfn 8943  ℂcc 11098  ℝcr 11099  0cc0 11100   + caddc 11103   ≤ cle 11244   − cmin 11441  ℕ₀cn0 12504  ℤcz 12591  ...cfz 13535  Σcsu 15737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-inf2 9610  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177  ax-pre-sup 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3375  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-er 8694  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-sup 9402  df-oi 9472  df-card 9925  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-div 11872  df-nn 12234  df-2 12303  df-3 12304  df-n0 12505  df-z 12592  df-uz 12863  df-rp 13017  df-ico 13378  df-fz 13536  df-fzo 13683  df-seq 14038  df-exp 14098  df-hash 14367  df-cj 15150  df-re 15151  df-im 15152  df-sqrt 15286  df-abs 15287  df-clim 15539  df-sum 15738

This theorem is referenced by:  dvnprodlem2  46588