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

Theorem dvnprodlem1 40635
Description: 𝐷 is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnprodlem1.c 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
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.
StepHypRef Expression
1 eqidd 2803 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
2 0zd 11649 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3 dvnprodlem1.j . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℕ0)
43nn0zd 11740 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ ℤ)
54adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6 fzssz 12560 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℤ
76a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℤ)
8 dvnprodlem1.c . . . . . . . . . . . . . . . . . . . . . . 23 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
98a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})))
10 oveq2 6876 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})))
11 rabeq 3378 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
1210, 11syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
13 sumeq1 14636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
1413eqeq1d 2804 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
1514rabbidv 3375 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1612, 15eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1716mpteq2dv 4932 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
1817adantl 469 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠 = (𝑅 ∪ {𝑍})) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
19 dvnprodlem1.rzt . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
20 dvnprodlem1.t . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑇 ∈ Fin)
21 ssexg 4993 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∪ {𝑍}) ⊆ 𝑇𝑇 ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ V)
2219, 20, 21syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
23 elpwg 4353 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
2519, 24mpbird 248 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
26 nn0ex 11559 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
2726mptex 6705 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
2827a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
299, 18, 25, 28fvmptd 6503 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
30 oveq2 6876 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
3130oveq1d 6883 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝐽 → ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
32 rabeq 3378 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
34 eqeq2 2813 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
3534rabbidv 3375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
3633, 35eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
3736adantl 469 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
38 ovex 6900 . . . . . . . . . . . . . . . . . . . . . . 23 ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∈ V
3938rabex 5001 . . . . . . . . . . . . . . . . . . . . . 22 {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
4039a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
4129, 37, 3, 40fvmptd 6503 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
42 ssrab2 3878 . . . . . . . . . . . . . . . . . . . . 21 {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍}))
4342a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
4441, 43eqsstrd 3830 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
4544adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
46 simpr 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
4745, 46sseldd 3793 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
48 elmapi 8108 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
4947, 48syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
50 dvnprodlem1.z . . . . . . . . . . . . . . . . . . 19 (𝜑𝑍𝑇)
51 snidg 4394 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑇𝑍 ∈ {𝑍})
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ {𝑍})
53 elun2 3974 . . . . . . . . . . . . . . . . . 18 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
5452, 53syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
5554adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
5649, 55ffvelrnd 6576 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
577, 56sseldd 3793 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℤ)
585, 57zsubcld 11747 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
592, 5, 583jca 1151 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ))
60 elfzle2 12562 . . . . . . . . . . . . . 14 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
6156, 60syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ≤ 𝐽)
625zred 11742 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
6357zred 11742 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℝ)
6462, 63subge0d 10896 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
6561, 64mpbird 248 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
66 elfzle1 12561 . . . . . . . . . . . . . 14 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
6756, 66syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐𝑍))
6862, 63subge02d 10898 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
6967, 68mpbid 223 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
7059, 65, 69jca32 507 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
71 elfz2 12550 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
7270, 71sylibr 225 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
73 elmapfn 8109 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
7447, 73syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
75 ssun1 3969 . . . . . . . . . . . . . . . . . 18 𝑅 ⊆ (𝑅 ∪ {𝑍})
7675a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
77 fnssres 6209 . . . . . . . . . . . . . . . . 17 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑅 ⊆ (𝑅 ∪ {𝑍})) → (𝑐𝑅) Fn 𝑅)
7874, 76, 77syl2anc 575 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) Fn 𝑅)
79 nfv 2005 . . . . . . . . . . . . . . . . . 18 𝑡𝜑
80 nfcv 2944 . . . . . . . . . . . . . . . . . . 19 𝑡𝑐
81 nfcv 2944 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝒫 𝑇
82 nfcv 2944 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡0
83 nfcv 2944 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡𝑠
8483nfsum1 14637 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡Σ𝑡𝑠 (𝑐𝑡)
85 nfcv 2944 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡𝑛
8684, 85nfeq 2956 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡Σ𝑡𝑠 (𝑐𝑡) = 𝑛
87 nfcv 2944 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡((0...𝑛) ↑𝑚 𝑠)
8886, 87nfrab 3308 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡{𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}
8982, 88nfmpt 4933 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
9081, 89nfmpt 4933 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
918, 90nfcxfr 2942 . . . . . . . . . . . . . . . . . . . . 21 𝑡𝐶
92 nfcv 2944 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝑅 ∪ {𝑍})
9391, 92nffv 6412 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝐶‘(𝑅 ∪ {𝑍}))
94 nfcv 2944 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐽
9593, 94nffv 6412 . . . . . . . . . . . . . . . . . . 19 𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
9680, 95nfel 2957 . . . . . . . . . . . . . . . . . 18 𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
9779, 96nfan 1990 . . . . . . . . . . . . . . . . 17 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
98 fvres 6421 . . . . . . . . . . . . . . . . . . . 20 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
9998adantl 469 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
1002adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ∈ ℤ)
10158adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
1026a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℤ)
10349adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
10476sselda 3792 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
105103, 104ffvelrnd 6576 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
106102, 105sseldd 3793 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℤ)
107100, 101, 1063jca 1151 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ))
108 elfzle1 12561 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐𝑡))
109105, 108syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ≤ (𝑐𝑡))
11019unssad 3983 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑅𝑇)
111 ssfi 8413 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
11220, 110, 111syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ Fin)
113112ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑅 ∈ Fin)
114 zssre 11644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℤ ⊆ ℝ
1156, 114sstri 3801 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0...𝐽) ⊆ ℝ
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (0...𝐽) ⊆ ℝ)
11749adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
11876sselda 3792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
119117, 118ffvelrnd 6576 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ (0...𝐽))
120116, 119sseldd 3793 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
121120adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
122 elfzle1 12561 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐𝑟))
123119, 122syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
124123adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
125 fveq2 6402 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 = 𝑡 → (𝑐𝑟) = (𝑐𝑡))
126 simpr 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑅)
127113, 121, 124, 125, 126fsumge1 14745 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ Σ𝑟𝑅 (𝑐𝑟))
128112adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
129120recnd 10347 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℂ)
130128, 129fsumcl 14681 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) ∈ ℂ)
13163recnd 10347 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
132130, 131pncand 10672 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) − (𝑐𝑍)) = Σ𝑟𝑅 (𝑐𝑟))
133 nfv 2005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑟(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
134 nfcv 2944 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑟(𝑐𝑍)
13550adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
136 dvnprodlem1.zr . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ¬ 𝑍𝑅)
137136adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
138 fveq2 6402 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑟 = 𝑍 → (𝑐𝑟) = (𝑐𝑍))
139133, 134, 128, 135, 137, 129, 138, 131fsumsplitsn 14691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)))
140139eqcomd 2808 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟))
141125cbvsumv 14643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡)
142141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
14341adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
14446, 143eleqtrd 2883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
145 rabid 3300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
146144, 145sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
147146simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽)
148142, 147eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = 𝐽)
149140, 148eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = 𝐽)
150149oveq1d 6883 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) − (𝑐𝑍)) = (𝐽 − (𝑐𝑍)))
151132, 150eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
152151adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
153127, 152breqtrd 4863 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))
154107, 109, 153jca32 507 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐𝑡) ∧ (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))))
155 elfz2 12550 . . . . . . . . . . . . . . . . . . . 20 ((𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))) ↔ ((0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐𝑡) ∧ (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))))
156154, 155sylibr 225 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
15799, 156eqeltrd 2881 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
158157ex 399 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
15997, 158ralrimi 3141 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
16078, 159jca 503 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
161 ffnfv 6604 . . . . . . . . . . . . . . 15 ((𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))) ↔ ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
162160, 161sylibr 225 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))))
163 ovexd 6902 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐𝑍))) ∈ V)
16420, 110ssexd 4994 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ V)
165164adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ V)
166163, 165elmapd 8100 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ↔ (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍)))))
167162, 166mpbird 248 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅))
16898a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡)))
16997, 168ralrimi 3141 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
170169sumeq2d 14649 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = Σ𝑡𝑅 (𝑐𝑡))
171125cbvsumv 14643 . . . . . . . . . . . . . . . 16 Σ𝑟𝑅 (𝑐𝑟) = Σ𝑡𝑅 (𝑐𝑡)
172171eqcomi 2811 . . . . . . . . . . . . . . 15 Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟)
173172a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟))
174151idi 2 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
175170, 173, 1743eqtrd 2840 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍)))
176167, 175jca 503 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
177 eqidd 2803 . . . . . . . . . . . . . . 15 (𝑒 = (𝑐𝑅) → 𝑅 = 𝑅)
178 simpl 470 . . . . . . . . . . . . . . . 16 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → 𝑒 = (𝑐𝑅))
179178fveq1d 6404 . . . . . . . . . . . . . . 15 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → (𝑒𝑡) = ((𝑐𝑅)‘𝑡))
180177, 179sumeq12rdv 14655 . . . . . . . . . . . . . 14 (𝑒 = (𝑐𝑅) → Σ𝑡𝑅 (𝑒𝑡) = Σ𝑡𝑅 ((𝑐𝑅)‘𝑡))
181180eqeq1d 2804 . . . . . . . . . . . . 13 (𝑒 = (𝑐𝑅) → (Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍)) ↔ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
182181elrab 3555 . . . . . . . . . . . 12 ((𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ↔ ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
183176, 182sylibr 225 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
184 oveq2 6876 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑅 → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑅))
185 rabeq 3378 . . . . . . . . . . . . . . . . . . . 20 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
186184, 185syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
187 sumeq1 14636 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
188187eqeq1d 2804 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
189188rabbidv 3375 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
190186, 189eqtrd 2836 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
191190mpteq2dv 4932 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
192191adantl 469 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 = 𝑅) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
193 elpwg 4353 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
194164, 193syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
195110, 194mpbird 248 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ 𝒫 𝑇)
19626mptex 6705 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
197196a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
1989, 192, 195, 197fvmptd 6503 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
199198adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
200 oveq2 6876 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
201200oveq1d 6883 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → ((0...𝑛) ↑𝑚 𝑅) = ((0...𝑚) ↑𝑚 𝑅))
202 rabeq 3378 . . . . . . . . . . . . . . . . . 18 (((0...𝑛) ↑𝑚 𝑅) = ((0...𝑚) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
203201, 202syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
204 eqeq2 2813 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑚))
205204rabbidv 3375 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
206203, 205eqtrd 2836 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
207206cbvmptv 4937 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
208207a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
209199, 208eqtrd 2836 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
210 fveq1 6401 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → (𝑐𝑡) = (𝑒𝑡))
211210sumeq2ad 14651 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑒 → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 (𝑒𝑡))
212211eqeq1d 2804 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = 𝑚))
213212cbvrabv 3385 . . . . . . . . . . . . . . . 16 {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚}
214213a1i 11 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
215 oveq2 6876 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝐽 − (𝑐𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐𝑍))))
216215oveq1d 6883 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐽 − (𝑐𝑍)) → ((0...𝑚) ↑𝑚 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅))
217 rabeq 3378 . . . . . . . . . . . . . . . 16 (((0...𝑚) ↑𝑚 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
218216, 217syl 17 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
219 eqeq2 2813 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐽 − (𝑐𝑍)) → (Σ𝑡𝑅 (𝑒𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))))
220219rabbidv 3375 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
221214, 218, 2203eqtrd 2840 . . . . . . . . . . . . . 14 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
222221adantl 469 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑚 = (𝐽 − (𝑐𝑍))) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
22358, 65jca 503 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
224 elnn0z 11650 . . . . . . . . . . . . . 14 ((𝐽 − (𝑐𝑍)) ∈ ℕ0 ↔ ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
225223, 224sylibr 225 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
226 ovex 6900 . . . . . . . . . . . . . . 15 ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∈ V
227226rabex 5001 . . . . . . . . . . . . . 14 {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V
228227a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V)
229209, 222, 225, 228fvmptd 6503 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
230229eqcomd 2808 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
231183, 230eleqtrd 2883 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
23272, 231jca 503 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
2331, 232jca 503 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
234 ovexd 6902 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ V)
235 vex 3390 . . . . . . . . . . 11 𝑐 ∈ V
236235resex 5642 . . . . . . . . . 10 (𝑐𝑅) ∈ V
237236a1i 11 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ V)
238 opeq12 4590 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
239238eqeq2d 2812 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
240 eleq1 2869 . . . . . . . . . . . . 13 (𝑘 = (𝐽 − (𝑐𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
241240adantr 468 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
242 simpr 473 . . . . . . . . . . . . 13 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → 𝑑 = (𝑐𝑅))
243 fveq2 6402 . . . . . . . . . . . . . 14 (𝑘 = (𝐽 − (𝑐𝑍)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
244243adantr 468 . . . . . . . . . . . . 13 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
245242, 244eleq12d 2875 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑑 ∈ ((𝐶𝑅)‘𝑘) ↔ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
246241, 245anbi12d 618 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
247239, 246anbi12d 618 . . . . . . . . . 10 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))))
248247spc2egv 3484 . . . . . . . . 9 (((𝐽 − (𝑐𝑍)) ∈ V ∧ (𝑐𝑅) ∈ V) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
249234, 237, 248syl2anc 575 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
250233, 249mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
251 eliunxp 5455 . . . . . . 7 (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
252250, 251sylibr 225 . . . . . 6 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
253 dvnprodlem1.d . . . . . 6 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
254252, 253fmptd 6600 . . . . 5 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
25595nfcri 2938 . . . . . . . . . . . 12 𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
25696, 255nfan 1990 . . . . . . . . . . 11 𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
25779, 256nfan 1990 . . . . . . . . . 10 𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
258 nfv 2005 . . . . . . . . . 10 𝑡(𝐷𝑐) = (𝐷𝑒)
259257, 258nfan 1990 . . . . . . . . 9 𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒))
26099eqcomd 2808 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
261260adantlrr 703 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
262261adantlr 697 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
263253a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
264 opex 5116 . . . . . . . . . . . . . . . . . . . 20 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
265264a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
266263, 265fvmpt2d 6508 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
267266fveq2d 6406 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
268267fveq1d 6404 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡))
269 ovex 6900 . . . . . . . . . . . . . . . . . . 19 (𝐽 − (𝑐𝑍)) ∈ V
270269, 236op2nd 7401 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝑐𝑅)
271270fveq1i 6403 . . . . . . . . . . . . . . . . 17 ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡)
272271a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡))
273268, 272eqtr2d 2837 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
274273adantrr 699 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
275274ad2antrr 708 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
276 simpr 473 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = (𝐷𝑒))
277253a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
278 fveq1 6401 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑒 → (𝑐𝑍) = (𝑒𝑍))
279278oveq2d 6884 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝑒𝑍)))
280 reseq1 5585 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝑐𝑅) = (𝑒𝑅))
281279, 280opeq12d 4596 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
282281adantl 469 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑐 = 𝑒) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
283 simpr 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
284 opex 5116 . . . . . . . . . . . . . . . . . . . . . . 23 ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V
285284a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V)
286277, 282, 283, 285fvmptd 6503 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
287286adantr 468 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
288276, 287eqtrd 2836 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
289288fveq2d 6406 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
290289adantlrl 702 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
291290adantr 468 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
292 ovex 6900 . . . . . . . . . . . . . . . . . 18 (𝐽 − (𝑒𝑍)) ∈ V
293 vex 3390 . . . . . . . . . . . . . . . . . . 19 𝑒 ∈ V
294293resex 5642 . . . . . . . . . . . . . . . . . 18 (𝑒𝑅) ∈ V
295292, 294op2nd 7401 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅)
296295a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅))
297291, 296eqtrd 2836 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (𝑒𝑅))
298297fveq1d 6404 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((𝑒𝑅)‘𝑡))
299 fvres 6421 . . . . . . . . . . . . . . 15 (𝑡𝑅 → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
300299adantl 469 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
301298, 300eqtrd 2836 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = (𝑒𝑡))
302262, 275, 3013eqtrd 2840 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
303302adantlr 697 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
304 simpl 470 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
305 elunnel1 3947 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 ∈ {𝑍})
306 elsni 4381 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
307305, 306syl 17 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
308307adantll 696 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
309 simpr 473 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
310309fveq2d 6406 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑐𝑍))
3113nn0cnd 11613 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ ℂ)
312311adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
313312, 131nncand 10676 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
314313eqcomd 2808 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
315314adantrr 699 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
316315adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
317266fveq2d 6406 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑐)) = (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
318269, 236op1st 7400 . . . . . . . . . . . . . . . . . . . . 21 (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍))
319318a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍)))
320317, 319eqtr2d 2837 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) = (1st ‘(𝐷𝑐)))
321320oveq2d 6884 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
322321adantrr 699 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
323322adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
324 fveq2 6402 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷𝑐) = (𝐷𝑒) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
325324adantl 469 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
326286fveq2d 6406 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
327326adantr 468 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
328292, 294op1st 7400 . . . . . . . . . . . . . . . . . . . . 21 (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍))
329328a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍)))
330325, 327, 3293eqtrd 2840 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (𝐽 − (𝑒𝑍)))
331330oveq2d 6884 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝐽 − (𝐽 − (𝑒𝑍))))
332311adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
333 zsscn 11645 . . . . . . . . . . . . . . . . . . . . . . 23 ℤ ⊆ ℂ
3346, 333sstri 3801 . . . . . . . . . . . . . . . . . . . . . 22 (0...𝐽) ⊆ ℂ
335334a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
336 eleq1w 2864 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
337336anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
338 feq1 6231 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
339337, 338imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
340339, 49chvarv 2436 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
34154adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
342340, 341ffvelrnd 6576 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ (0...𝐽))
343335, 342sseldd 3793 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ ℂ)
344332, 343nncand 10676 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
345344adantr 468 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
346 eqidd 2803 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑒𝑍) = (𝑒𝑍))
347331, 345, 3463eqtrd 2840 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
348347adantlrl 702 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
349316, 323, 3483eqtrd 2840 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝑒𝑍))
350349adantr 468 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑍) = (𝑒𝑍))
351 fveq2 6402 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → (𝑒𝑡) = (𝑒𝑍))
352351eqcomd 2808 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑒𝑍) = (𝑒𝑡))
353352adantl 469 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑒𝑍) = (𝑒𝑡))
354310, 350, 3533eqtrd 2840 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
355354adantlr 697 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
356304, 308, 355syl2anc 575 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
357303, 356pm2.61dan 838 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) = (𝑒𝑡))
358357ex 399 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → (𝑐𝑡) = (𝑒𝑡)))
359259, 358ralrimi 3141 . . . . . . . 8 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡))
36074adantrr 699 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
361360adantr 468 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
362340ffnd 6251 . . . . . . . . . . 11 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
363362adantrl 698 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
364363adantr 468 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
365 eqfnfv 6527 . . . . . . . . 9 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
366361, 364, 365syl2anc 575 . . . . . . . 8 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
367359, 366mpbird 248 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 = 𝑒)
368367ex 399 . . . . . 6 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
369368ralrimivva 3155 . . . . 5 (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
370254, 369jca 503 . . . 4 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
371 dff13 6730 . . . 4 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
372370, 371sylibr 225 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
373 eliun 4709 . . . . . . . . . . 11 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
374373biimpi 207 . . . . . . . . . 10 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
375374adantl 469 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
376 nfv 2005 . . . . . . . . . . 11 𝑘𝜑
377 nfcv 2944 . . . . . . . . . . . 12 𝑘𝑝
378 nfiu1 4735 . . . . . . . . . . . 12 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
379377, 378nfel 2957 . . . . . . . . . . 11 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
380376, 379nfan 1990 . . . . . . . . . 10 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
381 nfv 2005 . . . . . . . . . 10 𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}
382 nfv 2005 . . . . . . . . . . . . . . . . 17 𝑡 𝑘 ∈ (0...𝐽)
383 nfcv 2944 . . . . . . . . . . . . . . . . . 18 𝑡𝑝
384 nfcv 2944 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑘}
385 nfcv 2944 . . . . . . . . . . . . . . . . . . . . 21 𝑡𝑅
38691, 385nffv 6412 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝐶𝑅)
387 nfcv 2944 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑘
388386, 387nffv 6412 . . . . . . . . . . . . . . . . . . 19 𝑡((𝐶𝑅)‘𝑘)
389384, 388nfxp 5337 . . . . . . . . . . . . . . . . . 18 𝑡({𝑘} × ((𝐶𝑅)‘𝑘))
390383, 389nfel 2957 . . . . . . . . . . . . . . . . 17 𝑡 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))
39179, 382, 390nf3an 1993 . . . . . . . . . . . . . . . 16 𝑡(𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
392 0zd 11649 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
3934adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
3943933ad2antl1 1229 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
395 iftrue 4279 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
396395adantl 469 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
397 fzssz 12560 . . . . . . . . . . . . . . . . . . . . . . 23 (0...𝑘) ⊆ ℤ
398397a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℤ)
399 simp1 1159 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
400 simp2 1160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
401 xp2nd 7425 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
4024013ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
403198adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
404 oveq2 6876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
405404oveq1d 6883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑘 → ((0...𝑛) ↑𝑚 𝑅) = ((0...𝑘) ↑𝑚 𝑅))
406 rabeq 3378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0...𝑛) ↑𝑚 𝑅) = ((0...𝑘) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
407405, 406syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
408 eqeq2 2813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
409408rabbidv 3375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
410407, 409eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
411410adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
412 elfznn0 12650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
413412adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
414 ovex 6900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((0...𝑘) ↑𝑚 𝑅) ∈ V
415414rabex 5001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V
416415a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
417403, 411, 413, 416fvmptd 6503 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
4184173adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
419402, 418eleqtrd 2883 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
420 elrabi 3550 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
4214203ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}) → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
422399, 400, 419, 421syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
423 elmapi 8108 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) → (2nd𝑝):𝑅⟶(0...𝑘))
424422, 423syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝑘))
425424adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2nd𝑝):𝑅⟶(0...𝑘))
426425ffvelrnda 6575 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
427398, 426sseldd 3793 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
428396, 427eqeltrd 2881 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
429 simpl 470 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
430307adantll 696 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
431 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡 = 𝑍) → 𝑡 = 𝑍)
432136adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡 = 𝑍) → ¬ 𝑍𝑅)
433431, 432eqneltrd 2900 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡 = 𝑍) → ¬ 𝑡𝑅)
434433iffalsed 4284 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4354343ad2antl1 1229 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4364adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡 = 𝑍) → 𝐽 ∈ ℤ)
4374363ad2antl1 1229 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
438 xp1st 7424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
439 elsni 4381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
440438, 439syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
441440adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
4426sseli 3788 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
443442adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
444441, 443eqeltrd 2881 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
4454443adant1 1153 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
446445adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1st𝑝) ∈ ℤ)
447437, 446zsubcld 11747 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) ∈ ℤ)
448435, 447eqeltrd 2881 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
449448adantlr 697 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
450429, 430, 449syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
451428, 450pm2.61dan 838 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
452392, 394, 4513jca 1151 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ))
453424ffvelrnda 6575 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
454 elfzle1 12561 . . . . . . . . . . . . . . . . . . . . . 22 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2nd𝑝)‘𝑡))
455453, 454syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ ((2nd𝑝)‘𝑡))
456395eqcomd 2808 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝑅 → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
457456adantl 469 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
458455, 457breqtrd 4863 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
459458adantlr 697 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
460 simpll 774 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))))
461 elfzle2 12562 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
462 elfzel2 12557 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
463462zred 11742 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
464115sseli 3788 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
465463, 464subge0d 10896 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
466461, 465mpbird 248 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
467466adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
4684673ad2antl2 1230 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
469399, 433sylan 571 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡𝑅)
470469iffalsed 4284 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4714413adant1 1153 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
472471oveq2d 6884 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
473472adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
474470, 473eqtr2d 2837 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
475468, 474breqtrd 4863 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
476460, 430, 475syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
477459, 476pm2.61dan 838 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
478 simpl2 1237 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑘 ∈ (0...𝐽))
479397sseli 3788 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℤ)
480479zred 11742 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℝ)
481480adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ∈ ℝ)
482464adantl 469 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
483463adantl 469 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
484 elfzle2 12562 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
485484adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
486461adantl 469 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
487481, 482, 483, 485, 486letrd 10473 . . . . . . . . . . . . . . . . . . . . . 22 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
488453, 478, 487syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
489488adantlr 697 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
490396, 489eqbrtrd 4859 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
491474eqcomd 2808 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽𝑘))
492413nn0ge0d 11614 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
493463adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
494464adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
495493, 494subge02d 10898 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
496492, 495mpbid 223 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ≤ 𝐽)
497496adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
4984973adantl3 1202 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
499491, 498eqbrtrd 4859 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
500460, 430, 499syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
501490, 500pm2.61dan 838 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
502452, 477, 501jca32 507 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)))
503 elfz2 12550 . . . . . . . . . . . . . . . . 17 (if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)))
504502, 503sylibr 225 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽))
505 eqid 2802 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
506391, 504, 505fmptdf 6603 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
507 ovexd 6902 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ∈ V)
508399, 22syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
509507, 508elmapd 8100 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ↔ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽)))
510506, 509mpbird 248 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
511 eqidd 2803 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
512 eleq1w 2864 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑡 → (𝑟𝑅𝑡𝑅))
513 fveq2 6402 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑡 → ((2nd𝑝)‘𝑟) = ((2nd𝑝)‘𝑡))
514512, 513ifbieq1d 4296 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = 𝑡 → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
515514adantl 469 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑟 = 𝑡) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
516 simpr 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
517511, 515, 516, 451fvmptd 6503 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
518517ex 399 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
519391, 518ralrimi 3141 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
520519sumeq2d 14649 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
521 nfcv 2944 . . . . . . . . . . . . . . . 16 𝑡if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))
522399, 112syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
523399, 50syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
524399, 136syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
525395adantl 469 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
526453, 479syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
527526zcnd 11743 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℂ)
528525, 527eqeltrd 2881 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℂ)
529 eleq1 2869 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑍 → (𝑡𝑅𝑍𝑅))
530 fveq2 6402 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑍 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑍))
531529, 530ifbieq1d 4296 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))))
532136adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
533532iffalsed 4284 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
5345333adant2 1154 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
53543ad2ant1 1156 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
536535, 445zsubcld 11747 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℤ)
537536zcnd 11743 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℂ)
538534, 537eqeltrd 2881 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) ∈ ℂ)
539391, 521, 522, 523, 524, 528, 531, 538fsumsplitsn 14691 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))))
540395a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡)))
541391, 540ralrimi 3141 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
542541sumeq2d 14649 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
543 eqidd 2803 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (2nd𝑝) → 𝑅 = 𝑅)
544 simpl 470 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → 𝑐 = (2nd𝑝))
545544fveq1d 6404 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → (𝑐𝑡) = ((2nd𝑝)‘𝑡))
546543, 545sumeq12rdv 14655 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = (2nd𝑝) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
547546eqeq1d 2804 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (2nd𝑝) → (Σ𝑡𝑅 (𝑐𝑡) = 𝑘 ↔ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
548547elrab 3555 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ↔ ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
549419, 548sylib 209 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
550549simprd 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘)
551542, 550eqtrd 2836 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = 𝑘)
552524iffalsed 4284 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
553552, 472eqtrd 2836 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽𝑘))
554551, 553oveq12d 6886 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = (𝑘 + (𝐽𝑘)))
555334sseli 3788 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
5565553ad2ant2 1157 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
557399, 311syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
558556, 557pncan3d 10674 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 + (𝐽𝑘)) = 𝐽)
559554, 558eqtrd 2836 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = 𝐽)
560520, 539, 5593eqtrd 2840 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽)
561510, 560jca 503 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
562 eleq1w 2864 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑟 → (𝑡𝑅𝑟𝑅))
563 fveq2 6402 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑟 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑟))
564562, 563ifbieq1d 4296 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑟 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
565564cbvmptv 4937 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
566565eqeq2i 2814 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
567566biimpi 207 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
568 fveq1 6401 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → (𝑐𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
569568sumeq2ad 14651 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
570567, 569syl 17 . . . . . . . . . . . . . . 15 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
571570eqeq1d 2804 . . . . . . . . . . . . . 14 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
572571elrab 3555 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
573561, 572sylibr 225 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
5745733exp 1141 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
575574adantr 468 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
576380, 381, 575rexlimd 3210 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}))
577375, 576mpd 15 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
57841eqcomd 2808 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
579578adantr 468 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
580577, 579eleqtrd 2883 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
581253a1i 11 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
582 simpr 473 . . . . . . . . . . . . . . 15 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
583565a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
584582, 583eqtrd 2836 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
585 simpr 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 = 𝑍) → 𝑟 = 𝑍)
586136adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 = 𝑍) → ¬ 𝑍𝑅)
587585, 586eqneltrd 2900 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑍) → ¬ 𝑟𝑅)
588587iffalsed 4284 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
589588adantlr 697 . . . . . . . . . . . . . 14 (((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
59054adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
591 ovexd 6902 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (1st𝑝)) ∈ V)
592584, 589, 590, 591fvmptd 6503 . . . . . . . . . . . . 13 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑍) = (𝐽 − (1st𝑝)))
593592oveq2d 6884 . . . . . . . . . . . 12 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
594593adantlr 697 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
595311ad2antrr 708 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝐽 ∈ ℂ)
596 nfv 2005 . . . . . . . . . . . . . . . . 17 𝑘(1st𝑝) ∈ (0...𝐽)
597 simpl 470 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
598 simpr 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → (1st𝑝) = 𝑘)
599 simpl 470 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → 𝑘 ∈ (0...𝐽))
600598, 599eqeltrd 2881 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → (1st𝑝) ∈ (0...𝐽))
601597, 441, 600syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
602601ex 399 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
603602a1i 11 . . . . . . . . . . . . . . . . 17 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
604379, 596, 603rexlimd 3210 . . . . . . . . . . . . . . . 16 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
605374, 604mpd 15 . . . . . . . . . . . . . . 15 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))
6066sseli 3788 . . . . . . . . . . . . . . 15 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
607605, 606syl 17 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℤ)
608607zcnd 11743 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℂ)
609608ad2antlr 709 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (1st𝑝) ∈ ℂ)
610595, 609nncand 10676 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝐽 − (1st𝑝))) = (1st𝑝))
611594, 610eqtrd 2836 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (1st𝑝))
612 reseq1 5585 . . . . . . . . . . . 12 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
613612adantl 469 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
61475a1i 11 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
615614resmptd 5651 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅) = (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
616 nfv 2005 . . . . . . . . . . . . . 14 𝑘(𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)
617395mpteq2ia 4927 . . . . . . . . . . . . . . . . . 18 (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡))
618617a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
619424feqmptd 6464 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
620618, 619eqtr4d 2839 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
6216203exp 1141 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
622621adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
623380, 616, 622rexlimd 3210 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)))
624375, 623mpd 15 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
625624adantr 468 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
626613, 615, 6253eqtrd 2840 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = (2nd𝑝))
627611, 626opeq12d 4596 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
628 opex 5116 . . . . . . . . . 10 ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V
629628a1i 11 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V)
630581, 627, 580, 629fvmptd 6503 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) = ⟨(1st𝑝), (2nd𝑝)⟩)
631 nfv 2005 . . . . . . . . . 10 𝑘⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝
632 1st2nd2 7431 . . . . . . . . . . . . 13 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
633632eqcomd 2808 . . . . . . . . . . . 12 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
634633a1i 11 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
635634a1i 11 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)))
636380, 631, 635rexlimd 3210 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
637375, 636mpd 15 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
638630, 637eqtr2d 2837 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
639 fveq2 6402 . . . . . . . 8 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝐷𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
640639rspceeqv 3516 . . . . . . 7 (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
641580, 638, 640syl2anc 575 . . . . . 6 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
642641ralrimiva 3150 . . . . 5 (𝜑 → ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
643254, 642jca 503 . . . 4 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
644 dffo3 6590 . . . 4 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
645643, 644sylibr 225 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
646372, 645jca 503 . 2 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
647 df-f1o 6102 . 2 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
648646, 647sylibr 225 1 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2155  wral 3092  wrex 3093  {crab 3096  Vcvv 3387  cun 3761  wss 3763  ifcif 4273  𝒫 cpw 4345  {csn 4364  cop 4370   ciun 4705   class class class wbr 4837  cmpt 4916   × cxp 5303  cres 5307   Fn wfn 6090  wf 6091  1-1wf1 6092  ontowfo 6093  1-1-ontowf1o 6094  cfv 6095  (class class class)co 6868  1st c1st 7390  2nd c2nd 7391  𝑚 cmap 8086  Fincfn 8186  cc 10213  cr 10214  0cc0 10215   + caddc 10218  cle 10354  cmin 10545  0cn0 11553  cz 11637  ...cfz 12543  Σcsu 14633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-inf2 8779  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292  ax-pre-sup 10293
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-se 5265  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-isom 6104  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-om 7290  df-1st 7392  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-1o 7790  df-oadd 7794  df-er 7973  df-map 8088  df-en 8187  df-dom 8188  df-sdom 8189  df-fin 8190  df-sup 8581  df-oi 8648  df-card 9042  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-2 11358  df-3 11359  df-n0 11554  df-z 11638  df-uz 11899  df-rp 12041  df-ico 12393  df-fz 12544  df-fzo 12684  df-seq 13019  df-exp 13078  df-hash 13332  df-cj 14056  df-re 14057  df-im 14058  df-sqrt 14192  df-abs 14193  df-clim 14436  df-sum 14634
This theorem is referenced by:  dvnprodlem2  40636
  Copyright terms: Public domain W3C validator