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 38836
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 2611 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
2 0zd 11266 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3 dvnprodlem1.j . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℕ0)
43nn0zd 11356 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ ℤ)
54adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6 fzssz 12214 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℤ
76a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℤ)
8 dvnprodlem1.c . . . . . . . . . . . . . . . . . . . . . . 23 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
98a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})))
10 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})))
11 rabeq 3166 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
1210, 11syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
13 sumeq1 14267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
1413eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
1514rabbidv 3164 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1612, 15eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1716mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
1817adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠 = (𝑅 ∪ {𝑍})) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
19 dvnprodlem1.rzt . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
20 dvnprodlem1.t . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑇 ∈ Fin)
21 ssexg 4732 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∪ {𝑍}) ⊆ 𝑇𝑇 ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ V)
2219, 20, 21syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
23 elpwg 4116 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
2519, 24mpbird 246 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
26 nn0ex 11175 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
2726mptex 6390 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
2827a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
299, 18, 25, 28fvmptd 6197 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
30 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
3130oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝐽 → ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
32 rabeq 3166 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
34 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
3534rabbidv 3164 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
3633, 35eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
3736adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
38 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . 23 ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∈ V
3938rabex 4740 . . . . . . . . . . . . . . . . . . . . . 22 {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
4039a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
4129, 37, 3, 40fvmptd 6197 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
42 ssrab2 3650 . . . . . . . . . . . . . . . . . . . . 21 {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍}))
4342a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
4441, 43eqsstrd 3602 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
4544adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
46 simpr 476 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
4745, 46sseldd 3569 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
48 elmapi 7765 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
4947, 48syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
50 dvnprodlem1.z . . . . . . . . . . . . . . . . . . 19 (𝜑𝑍𝑇)
51 snidg 4153 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑇𝑍 ∈ {𝑍})
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ {𝑍})
53 elun2 3743 . . . . . . . . . . . . . . . . . 18 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
5452, 53syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
5554adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
5649, 55ffvelrnd 6268 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
577, 56sseldd 3569 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℤ)
585, 57zsubcld 11363 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
592, 5, 583jca 1235 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ))
60 elfzle2 12216 . . . . . . . . . . . . . 14 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
6156, 60syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ≤ 𝐽)
625zred 11358 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
6357zred 11358 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℝ)
6462, 63subge0d 10496 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
6561, 64mpbird 246 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
66 elfzle1 12215 . . . . . . . . . . . . . 14 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
6756, 66syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐𝑍))
6862, 63subge02d 10498 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
6967, 68mpbid 221 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
7059, 65, 69jca32 556 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
71 elfz2 12204 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
7270, 71sylibr 223 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
73 elmapfn 7766 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
7447, 73syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
75 ssun1 3738 . . . . . . . . . . . . . . . . . 18 𝑅 ⊆ (𝑅 ∪ {𝑍})
7675a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
77 fnssres 5918 . . . . . . . . . . . . . . . . 17 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑅 ⊆ (𝑅 ∪ {𝑍})) → (𝑐𝑅) Fn 𝑅)
7874, 76, 77syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) Fn 𝑅)
79 nfv 1830 . . . . . . . . . . . . . . . . . 18 𝑡𝜑
80 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 𝑡𝑐
81 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝒫 𝑇
82 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡0
83 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡𝑠
8483nfsum1 14268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡Σ𝑡𝑠 (𝑐𝑡)
85 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡𝑛
8684, 85nfeq 2762 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡Σ𝑡𝑠 (𝑐𝑡) = 𝑛
87 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡((0...𝑛) ↑𝑚 𝑠)
8886, 87nfrab 3100 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡{𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}
8982, 88nfmpt 4674 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
9081, 89nfmpt 4674 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
918, 90nfcxfr 2749 . . . . . . . . . . . . . . . . . . . . 21 𝑡𝐶
92 nfcv 2751 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝑅 ∪ {𝑍})
9391, 92nffv 6110 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝐶‘(𝑅 ∪ {𝑍}))
94 nfcv 2751 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐽
9593, 94nffv 6110 . . . . . . . . . . . . . . . . . . 19 𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
9680, 95nfel 2763 . . . . . . . . . . . . . . . . . 18 𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
9779, 96nfan 1816 . . . . . . . . . . . . . . . . 17 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
98 fvres 6117 . . . . . . . . . . . . . . . . . . . 20 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
9998adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
1002adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ∈ ℤ)
10158adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
1026a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℤ)
10349adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
10476sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
105103, 104ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
106102, 105sseldd 3569 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℤ)
107100, 101, 1063jca 1235 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ))
108 elfzle1 12215 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐𝑡))
109105, 108syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ≤ (𝑐𝑡))
11019unssad 3752 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑅𝑇)
111 ssfi 8065 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
11220, 110, 111syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ Fin)
113112ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑅 ∈ Fin)
114 zssre 11261 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℤ ⊆ ℝ
1156, 114sstri 3577 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0...𝐽) ⊆ ℝ
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (0...𝐽) ⊆ ℝ)
11749adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
11876sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
119117, 118ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ (0...𝐽))
120116, 119sseldd 3569 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
121120adantlr 747 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
122 elfzle1 12215 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐𝑟))
123119, 122syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
124123adantlr 747 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
125 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 = 𝑡 → (𝑐𝑟) = (𝑐𝑡))
126 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑅)
127113, 121, 124, 125, 126fsumge1 14370 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ Σ𝑟𝑅 (𝑐𝑟))
128112adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
129120recnd 9947 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℂ)
130128, 129fsumcl 14311 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) ∈ ℂ)
13163recnd 9947 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
132130, 131pncand 10272 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) − (𝑐𝑍)) = Σ𝑟𝑅 (𝑐𝑟))
133 nfv 1830 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑟(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
134 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑟(𝑐𝑍)
13550adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
136 dvnprodlem1.zr . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ¬ 𝑍𝑅)
137136adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
138 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑟 = 𝑍 → (𝑐𝑟) = (𝑐𝑍))
139133, 134, 128, 135, 137, 129, 138, 131fsumsplitsn 38637 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)))
140139eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟))
141125cbvsumv 14274 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡)
142141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
14341adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
14446, 143eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
145 rabid 3095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
146144, 145sylib 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
147146simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽)
148142, 147eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = 𝐽)
149140, 148eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = 𝐽)
150149oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) − (𝑐𝑍)) = (𝐽 − (𝑐𝑍)))
151132, 150eqtr3d 2646 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
152151adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
153127, 152breqtrd 4609 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))
154107, 109, 153jca32 556 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐𝑡) ∧ (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))))
155 elfz2 12204 . . . . . . . . . . . . . . . . . . . 20 ((𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))) ↔ ((0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐𝑡) ∧ (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))))
156154, 155sylibr 223 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
15799, 156eqeltrd 2688 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
158157ex 449 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
15997, 158ralrimi 2940 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
16078, 159jca 553 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
161 ffnfv 6295 . . . . . . . . . . . . . . 15 ((𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))) ↔ ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
162160, 161sylibr 223 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))))
163 ovex 6577 . . . . . . . . . . . . . . . 16 (0...(𝐽 − (𝑐𝑍))) ∈ V
164163a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐𝑍))) ∈ V)
16520, 110ssexd 4733 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ V)
166165adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ V)
167164, 166elmapd 7758 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ↔ (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍)))))
168162, 167mpbird 246 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅))
16998a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡)))
17097, 169ralrimi 2940 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
171170sumeq2d 14280 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = Σ𝑡𝑅 (𝑐𝑡))
172125cbvsumv 14274 . . . . . . . . . . . . . . . 16 Σ𝑟𝑅 (𝑐𝑟) = Σ𝑡𝑅 (𝑐𝑡)
173172eqcomi 2619 . . . . . . . . . . . . . . 15 Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟)
174173a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟))
175151idi 2 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
176171, 174, 1753eqtrd 2648 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍)))
177168, 176jca 553 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
178 eqidd 2611 . . . . . . . . . . . . . . 15 (𝑒 = (𝑐𝑅) → 𝑅 = 𝑅)
179 simpl 472 . . . . . . . . . . . . . . . 16 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → 𝑒 = (𝑐𝑅))
180179fveq1d 6105 . . . . . . . . . . . . . . 15 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → (𝑒𝑡) = ((𝑐𝑅)‘𝑡))
181178, 180sumeq12rdv 14285 . . . . . . . . . . . . . 14 (𝑒 = (𝑐𝑅) → Σ𝑡𝑅 (𝑒𝑡) = Σ𝑡𝑅 ((𝑐𝑅)‘𝑡))
182181eqeq1d 2612 . . . . . . . . . . . . 13 (𝑒 = (𝑐𝑅) → (Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍)) ↔ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
183182elrab 3331 . . . . . . . . . . . 12 ((𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ↔ ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
184177, 183sylibr 223 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
185 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑅 → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑅))
186 rabeq 3166 . . . . . . . . . . . . . . . . . . . 20 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
187185, 186syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
188 sumeq1 14267 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
189188eqeq1d 2612 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
190189rabbidv 3164 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
191187, 190eqtrd 2644 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
192191mpteq2dv 4673 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
193192adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 = 𝑅) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
194 elpwg 4116 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
195165, 194syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
196110, 195mpbird 246 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ 𝒫 𝑇)
19726mptex 6390 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
198197a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
1999, 193, 196, 198fvmptd 6197 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
200199adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
201 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
202201oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → ((0...𝑛) ↑𝑚 𝑅) = ((0...𝑚) ↑𝑚 𝑅))
203 rabeq 3166 . . . . . . . . . . . . . . . . . 18 (((0...𝑛) ↑𝑚 𝑅) = ((0...𝑚) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
204202, 203syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
205 eqeq2 2621 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑚))
206205rabbidv 3164 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
207204, 206eqtrd 2644 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
208207cbvmptv 4678 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
209208a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
210200, 209eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
211 fveq1 6102 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → (𝑐𝑡) = (𝑒𝑡))
212211sumeq2ad 38632 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑒 → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 (𝑒𝑡))
213212eqeq1d 2612 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = 𝑚))
214213cbvrabv 3172 . . . . . . . . . . . . . . . 16 {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚}
215214a1i 11 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
216 oveq2 6557 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝐽 − (𝑐𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐𝑍))))
217216oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐽 − (𝑐𝑍)) → ((0...𝑚) ↑𝑚 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅))
218 rabeq 3166 . . . . . . . . . . . . . . . 16 (((0...𝑚) ↑𝑚 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
219217, 218syl 17 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
220 eqeq2 2621 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐽 − (𝑐𝑍)) → (Σ𝑡𝑅 (𝑒𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))))
221220rabbidv 3164 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
222215, 219, 2213eqtrd 2648 . . . . . . . . . . . . . 14 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
223222adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑚 = (𝐽 − (𝑐𝑍))) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
22458, 65jca 553 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
225 elnn0z 11267 . . . . . . . . . . . . . 14 ((𝐽 − (𝑐𝑍)) ∈ ℕ0 ↔ ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
226224, 225sylibr 223 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
227 ovex 6577 . . . . . . . . . . . . . . 15 ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∈ V
228227rabex 4740 . . . . . . . . . . . . . 14 {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V
229228a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V)
230210, 223, 226, 229fvmptd 6197 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
231230eqcomd 2616 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
232184, 231eleqtrd 2690 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
23372, 232jca 553 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
2341, 233jca 553 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
235232elfvexd 6132 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ V)
236 vex 3176 . . . . . . . . . . 11 𝑐 ∈ V
237236resex 5363 . . . . . . . . . 10 (𝑐𝑅) ∈ V
238237a1i 11 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ V)
239 opeq12 4342 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
240239eqeq2d 2620 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
241 eleq1 2676 . . . . . . . . . . . . 13 (𝑘 = (𝐽 − (𝑐𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
242241adantr 480 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
243 simpr 476 . . . . . . . . . . . . 13 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → 𝑑 = (𝑐𝑅))
244 fveq2 6103 . . . . . . . . . . . . . 14 (𝑘 = (𝐽 − (𝑐𝑍)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
245244adantr 480 . . . . . . . . . . . . 13 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
246243, 245eleq12d 2682 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑑 ∈ ((𝐶𝑅)‘𝑘) ↔ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
247242, 246anbi12d 743 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
248240, 247anbi12d 743 . . . . . . . . . 10 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))))
249248spc2egv 3268 . . . . . . . . 9 (((𝐽 − (𝑐𝑍)) ∈ V ∧ (𝑐𝑅) ∈ V) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
250235, 238, 249syl2anc 691 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
251234, 250mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
252 eliunxp 5181 . . . . . . 7 (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
253251, 252sylibr 223 . . . . . 6 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
254 dvnprodlem1.d . . . . . 6 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
255253, 254fmptd 6292 . . . . 5 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
25695nfcri 2745 . . . . . . . . . . . 12 𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
25796, 256nfan 1816 . . . . . . . . . . 11 𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
25879, 257nfan 1816 . . . . . . . . . 10 𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
259 nfv 1830 . . . . . . . . . 10 𝑡(𝐷𝑐) = (𝐷𝑒)
260258, 259nfan 1816 . . . . . . . . 9 𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒))
26199eqcomd 2616 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
262261adantlrr 753 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
263262adantlr 747 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
264254a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
265 opex 4859 . . . . . . . . . . . . . . . . . . . 20 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
266265a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
267264, 266fvmpt2d 6202 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
268267fveq2d 6107 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
269268fveq1d 6105 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡))
270 ovex 6577 . . . . . . . . . . . . . . . . . . 19 (𝐽 − (𝑐𝑍)) ∈ V
271270, 237op2nd 7068 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝑐𝑅)
272271fveq1i 6104 . . . . . . . . . . . . . . . . 17 ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡)
273272a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡))
274269, 273eqtr2d 2645 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
275274adantrr 749 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
276275ad2antrr 758 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
277 simpr 476 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = (𝐷𝑒))
278254a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
279 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑒 → (𝑐𝑍) = (𝑒𝑍))
280279oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝑒𝑍)))
281 reseq1 5311 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝑐𝑅) = (𝑒𝑅))
282280, 281opeq12d 4348 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
283282adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑐 = 𝑒) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
284 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
285 opex 4859 . . . . . . . . . . . . . . . . . . . . . . 23 ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V
286285a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V)
287278, 283, 284, 286fvmptd 6197 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
288287adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
289277, 288eqtrd 2644 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
290289fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
291290adantlrl 752 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
292291adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
293 ovex 6577 . . . . . . . . . . . . . . . . . 18 (𝐽 − (𝑒𝑍)) ∈ V
294 vex 3176 . . . . . . . . . . . . . . . . . . 19 𝑒 ∈ V
295294resex 5363 . . . . . . . . . . . . . . . . . 18 (𝑒𝑅) ∈ V
296293, 295op2nd 7068 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅)
297296a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅))
298292, 297eqtrd 2644 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (𝑒𝑅))
299298fveq1d 6105 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((𝑒𝑅)‘𝑡))
300 fvres 6117 . . . . . . . . . . . . . . 15 (𝑡𝑅 → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
301300adantl 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
302299, 301eqtrd 2644 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = (𝑒𝑡))
303263, 276, 3023eqtrd 2648 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
304303adantlr 747 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
305 simpl 472 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
306 elunnel1 3716 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 ∈ {𝑍})
307 elsni 4142 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
308306, 307syl 17 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
309308adantll 746 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
310 simpr 476 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
311310fveq2d 6107 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑐𝑍))
3123nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ ℂ)
313312adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
314313, 131nncand 10276 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
315314eqcomd 2616 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
316315adantrr 749 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
317316adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
318267fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑐)) = (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
319270, 237op1st 7067 . . . . . . . . . . . . . . . . . . . . 21 (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍))
320319a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍)))
321318, 320eqtr2d 2645 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) = (1st ‘(𝐷𝑐)))
322321oveq2d 6565 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
323322adantrr 749 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
324323adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
325 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷𝑐) = (𝐷𝑒) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
326325adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
327287fveq2d 6107 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
328327adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
329293, 295op1st 7067 . . . . . . . . . . . . . . . . . . . . 21 (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍))
330329a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍)))
331326, 328, 3303eqtrd 2648 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (𝐽 − (𝑒𝑍)))
332331oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝐽 − (𝐽 − (𝑒𝑍))))
333312adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
334 zsscn 11262 . . . . . . . . . . . . . . . . . . . . . . 23 ℤ ⊆ ℂ
3356, 334sstri 3577 . . . . . . . . . . . . . . . . . . . . . 22 (0...𝐽) ⊆ ℂ
336335a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
337 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
338337anbi2d 736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
339 feq1 5939 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
340338, 339imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
341340, 49chvarv 2251 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
34254adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
343341, 342ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ (0...𝐽))
344336, 343sseldd 3569 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ ℂ)
345333, 344nncand 10276 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
346345adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
347 eqidd 2611 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑒𝑍) = (𝑒𝑍))
348332, 346, 3473eqtrd 2648 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
349348adantlrl 752 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
350317, 324, 3493eqtrd 2648 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝑒𝑍))
351350adantr 480 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑍) = (𝑒𝑍))
352 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → (𝑒𝑡) = (𝑒𝑍))
353352eqcomd 2616 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑒𝑍) = (𝑒𝑡))
354353adantl 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑒𝑍) = (𝑒𝑡))
355311, 351, 3543eqtrd 2648 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
356355adantlr 747 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
357305, 309, 356syl2anc 691 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
358304, 357pm2.61dan 828 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) = (𝑒𝑡))
359358ex 449 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → (𝑐𝑡) = (𝑒𝑡)))
360260, 359ralrimi 2940 . . . . . . . 8 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡))
36174adantrr 749 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
362361adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
363 ffn 5958 . . . . . . . . . . . 12 (𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽) → 𝑒 Fn (𝑅 ∪ {𝑍}))
364341, 363syl 17 . . . . . . . . . . 11 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
365364adantrl 748 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
366365adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
367 eqfnfv 6219 . . . . . . . . 9 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
368362, 366, 367syl2anc 691 . . . . . . . 8 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
369360, 368mpbird 246 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 = 𝑒)
370369ex 449 . . . . . 6 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
371370ralrimivva 2954 . . . . 5 (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
372255, 371jca 553 . . . 4 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
373 dff13 6416 . . . 4 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
374372, 373sylibr 223 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
375 eliun 4460 . . . . . . . . . . 11 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
376375biimpi 205 . . . . . . . . . 10 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
377376adantl 481 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
378 nfv 1830 . . . . . . . . . . 11 𝑘𝜑
379 nfcv 2751 . . . . . . . . . . . 12 𝑘𝑝
380 nfiu1 4486 . . . . . . . . . . . 12 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
381379, 380nfel 2763 . . . . . . . . . . 11 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
382378, 381nfan 1816 . . . . . . . . . 10 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
383 nfv 1830 . . . . . . . . . 10 𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}
384 nfv 1830 . . . . . . . . . . . . . . . . 17 𝑡 𝑘 ∈ (0...𝐽)
385 nfcv 2751 . . . . . . . . . . . . . . . . . 18 𝑡𝑝
386 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑘}
387 nfcv 2751 . . . . . . . . . . . . . . . . . . . . 21 𝑡𝑅
38891, 387nffv 6110 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝐶𝑅)
389 nfcv 2751 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑘
390388, 389nffv 6110 . . . . . . . . . . . . . . . . . . 19 𝑡((𝐶𝑅)‘𝑘)
391386, 390nfxp 5066 . . . . . . . . . . . . . . . . . 18 𝑡({𝑘} × ((𝐶𝑅)‘𝑘))
392385, 391nfel 2763 . . . . . . . . . . . . . . . . 17 𝑡 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))
39379, 384, 392nf3an 1819 . . . . . . . . . . . . . . . 16 𝑡(𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
394 0zd 11266 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
3954adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
3963953ad2antl1 1216 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
397 iftrue 4042 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
398397adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
399 fzssz 12214 . . . . . . . . . . . . . . . . . . . . . . 23 (0...𝑘) ⊆ ℤ
400399a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℤ)
401 simp1 1054 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
402 simp2 1055 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
403 xp2nd 7090 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
4044033ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
405199adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
406 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
407406oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑘 → ((0...𝑛) ↑𝑚 𝑅) = ((0...𝑘) ↑𝑚 𝑅))
408 rabeq 3166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0...𝑛) ↑𝑚 𝑅) = ((0...𝑘) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
409407, 408syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
410 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
411410rabbidv 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
412409, 411eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
413412adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
414 elfznn0 12302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
415414adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
416 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((0...𝑘) ↑𝑚 𝑅) ∈ V
417416rabex 4740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V
418417a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
419405, 413, 415, 418fvmptd 6197 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
4204193adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
421404, 420eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
422 elrabi 3328 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
4234223ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}) → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
424401, 402, 421, 423syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
425 elmapi 7765 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) → (2nd𝑝):𝑅⟶(0...𝑘))
426424, 425syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝑘))
427426adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2nd𝑝):𝑅⟶(0...𝑘))
428427ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
429400, 428sseldd 3569 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
430398, 429eqeltrd 2688 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
431 simpl 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
432308adantll 746 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
433 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡 = 𝑍) → 𝑡 = 𝑍)
434136adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡 = 𝑍) → ¬ 𝑍𝑅)
435433, 434eqneltrd 2707 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡 = 𝑍) → ¬ 𝑡𝑅)
436435iffalsed 4047 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4374363ad2antl1 1216 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4384adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡 = 𝑍) → 𝐽 ∈ ℤ)
4394383ad2antl1 1216 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
440 xp1st 7089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
441 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
442440, 441syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
443442adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
4446sseli 3564 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
445444adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
446443, 445eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
4474463adant1 1072 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
448447adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1st𝑝) ∈ ℤ)
449439, 448zsubcld 11363 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) ∈ ℤ)
450437, 449eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
451450adantlr 747 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
452431, 432, 451syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
453430, 452pm2.61dan 828 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
454394, 396, 4533jca 1235 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ))
455426ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
456 elfzle1 12215 . . . . . . . . . . . . . . . . . . . . . 22 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2nd𝑝)‘𝑡))
457455, 456syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ ((2nd𝑝)‘𝑡))
458397eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝑅 → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
459458adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
460457, 459breqtrd 4609 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
461460adantlr 747 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
462 simpll 786 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))))
463 elfzle2 12216 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
464 elfzel2 12211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
465464zred 11358 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
466115sseli 3564 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
467465, 466subge0d 10496 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
468463, 467mpbird 246 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
469468adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
4704693ad2antl2 1217 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
471401, 435sylan 487 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡𝑅)
472471iffalsed 4047 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4734433adant1 1072 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
474473oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
475474adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
476472, 475eqtr2d 2645 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
477470, 476breqtrd 4609 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
478462, 432, 477syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
479461, 478pm2.61dan 828 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
480 simpl2 1058 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑘 ∈ (0...𝐽))
481399sseli 3564 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℤ)
482481zred 11358 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℝ)
483482adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ∈ ℝ)
484466adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
485465adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
486 elfzle2 12216 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
487486adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
488463adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
489483, 484, 485, 487, 488letrd 10073 . . . . . . . . . . . . . . . . . . . . . 22 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
490455, 480, 489syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
491490adantlr 747 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
492398, 491eqbrtrd 4605 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
493476eqcomd 2616 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽𝑘))
494415nn0ge0d 11231 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
495465adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
496466adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
497495, 496subge02d 10498 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
498494, 497mpbid 221 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ≤ 𝐽)
499498adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
5004993adantl3 1212 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
501493, 500eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
502462, 432, 501syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
503492, 502pm2.61dan 828 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
504454, 479, 503jca32 556 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)))
505 elfz2 12204 . . . . . . . . . . . . . . . . 17 (if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)))
506504, 505sylibr 223 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽))
507 eqid 2610 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
508393, 506, 507fmptdf 6294 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
509 ovex 6577 . . . . . . . . . . . . . . . . 17 (0...𝐽) ∈ V
510509a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ∈ V)
511401, 22syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
512510, 511elmapd 7758 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ↔ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽)))
513508, 512mpbird 246 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
514 eqidd 2611 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
515 eleq1 2676 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑡 → (𝑟𝑅𝑡𝑅))
516 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑡 → ((2nd𝑝)‘𝑟) = ((2nd𝑝)‘𝑡))
517515, 516ifbieq1d 4059 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = 𝑡 → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
518517adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑟 = 𝑡) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
519 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
520514, 518, 519, 453fvmptd 6197 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
521520ex 449 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
522393, 521ralrimi 2940 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
523522sumeq2d 14280 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
524 nfcv 2751 . . . . . . . . . . . . . . . 16 𝑡if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))
525401, 112syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
526401, 50syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
527401, 136syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
528397adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
529455, 481syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
530529zcnd 11359 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℂ)
531528, 530eqeltrd 2688 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℂ)
532 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑍 → (𝑡𝑅𝑍𝑅))
533 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑍 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑍))
534532, 533ifbieq1d 4059 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))))
535136adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
536535iffalsed 4047 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
5375363adant2 1073 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
53843ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
539538, 447zsubcld 11363 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℤ)
540539zcnd 11359 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℂ)
541537, 540eqeltrd 2688 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) ∈ ℂ)
542393, 524, 525, 526, 527, 531, 534, 541fsumsplitsn 38637 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))))
543397a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡)))
544393, 543ralrimi 2940 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
545544sumeq2d 14280 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
546 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (2nd𝑝) → 𝑅 = 𝑅)
547 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → 𝑐 = (2nd𝑝))
548547fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → (𝑐𝑡) = ((2nd𝑝)‘𝑡))
549546, 548sumeq12rdv 14285 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = (2nd𝑝) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
550549eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (2nd𝑝) → (Σ𝑡𝑅 (𝑐𝑡) = 𝑘 ↔ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
551550elrab 3331 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ↔ ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
552421, 551sylib 207 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
553552simprd 478 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘)
554545, 553eqtrd 2644 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = 𝑘)
555527iffalsed 4047 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
556555, 474eqtrd 2644 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽𝑘))
557554, 556oveq12d 6567 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = (𝑘 + (𝐽𝑘)))
558335sseli 3564 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
5595583ad2ant2 1076 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
560401, 312syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
561559, 560pncan3d 10274 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 + (𝐽𝑘)) = 𝐽)
562557, 561eqtrd 2644 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = 𝐽)
563523, 542, 5623eqtrd 2648 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽)
564513, 563jca 553 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
565 eleq1 2676 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑟 → (𝑡𝑅𝑟𝑅))
566 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑟 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑟))
567565, 566ifbieq1d 4059 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑟 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
568567cbvmptv 4678 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
569568eqeq2i 2622 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
570569biimpi 205 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
571 fveq1 6102 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → (𝑐𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
572571sumeq2ad 38632 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
573570, 572syl 17 . . . . . . . . . . . . . . 15 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
574573eqeq1d 2612 . . . . . . . . . . . . . 14 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
575574elrab 3331 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
576564, 575sylibr 223 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
5775763exp 1256 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
578577adantr 480 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
579382, 383, 578rexlimd 3008 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}))
580377, 579mpd 15 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
58141eqcomd 2616 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
582581adantr 480 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
583580, 582eleqtrd 2690 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
584254a1i 11 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
585 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
586568a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
587585, 586eqtrd 2644 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
588 simpr 476 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 = 𝑍) → 𝑟 = 𝑍)
589136adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 = 𝑍) → ¬ 𝑍𝑅)
590588, 589eqneltrd 2707 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑍) → ¬ 𝑟𝑅)
591590iffalsed 4047 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
592591adantlr 747 . . . . . . . . . . . . . 14 (((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
59354adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
594 ovex 6577 . . . . . . . . . . . . . . 15 (𝐽 − (1st𝑝)) ∈ V
595594a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (1st𝑝)) ∈ V)
596587, 592, 593, 595fvmptd 6197 . . . . . . . . . . . . 13 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑍) = (𝐽 − (1st𝑝)))
597596oveq2d 6565 . . . . . . . . . . . 12 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
598597adantlr 747 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
599312ad2antrr 758 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝐽 ∈ ℂ)
600 nfv 1830 . . . . . . . . . . . . . . . . 17 𝑘(1st𝑝) ∈ (0...𝐽)
601 simpl 472 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
602 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → (1st𝑝) = 𝑘)
603 simpl 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → 𝑘 ∈ (0...𝐽))
604602, 603eqeltrd 2688 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → (1st𝑝) ∈ (0...𝐽))
605601, 443, 604syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
606605ex 449 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
607606a1i 11 . . . . . . . . . . . . . . . . 17 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
608381, 600, 607rexlimd 3008 . . . . . . . . . . . . . . . 16 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
609376, 608mpd 15 . . . . . . . . . . . . . . 15 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))
6106sseli 3564 . . . . . . . . . . . . . . 15 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
611609, 610syl 17 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℤ)
612611zcnd 11359 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℂ)
613612ad2antlr 759 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (1st𝑝) ∈ ℂ)
614599, 613nncand 10276 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝐽 − (1st𝑝))) = (1st𝑝))
615598, 614eqtrd 2644 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (1st𝑝))
616 reseq1 5311 . . . . . . . . . . . 12 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
617616adantl 481 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
61875a1i 11 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
619618resmptd 5371 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅) = (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
620 nfv 1830 . . . . . . . . . . . . . 14 𝑘(𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)
621397mpteq2ia 4668 . . . . . . . . . . . . . . . . . 18 (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡))
622621a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
623426feqmptd 6159 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
624622, 623eqtr4d 2647 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
6256243exp 1256 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
626625adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
627382, 620, 626rexlimd 3008 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)))
628377, 627mpd 15 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
629628adantr 480 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
630617, 619, 6293eqtrd 2648 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = (2nd𝑝))
631615, 630opeq12d 4348 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
632 opex 4859 . . . . . . . . . 10 ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V
633632a1i 11 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V)
634584, 631, 583, 633fvmptd 6197 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) = ⟨(1st𝑝), (2nd𝑝)⟩)
635 nfv 1830 . . . . . . . . . 10 𝑘⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝
636 1st2nd2 7096 . . . . . . . . . . . . 13 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
637636eqcomd 2616 . . . . . . . . . . . 12 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
638637a1i 11 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
639638a1i 11 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)))
640382, 635, 639rexlimd 3008 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
641377, 640mpd 15 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
642634, 641eqtr2d 2645 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
643 fveq2 6103 . . . . . . . . 9 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝐷𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
644643eqeq2d 2620 . . . . . . . 8 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝑝 = (𝐷𝑐) ↔ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))))
645644rspcev 3282 . . . . . . 7 (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
646583, 642, 645syl2anc 691 . . . . . 6 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
647646ralrimiva 2949 . . . . 5 (𝜑 → ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
648255, 647jca 553 . . . 4 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
649 dffo3 6282 . . . 4 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
650648, 649sylibr 223 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
651374, 650jca 553 . 2 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
652 df-f1o 5811 . 2 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
653651, 652sylibr 223 1 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wex 1695  wcel 1977  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  cun 3538  wss 3540  ifcif 4036  𝒫 cpw 4108  {csn 4125  cop 4131   ciun 4455   class class class wbr 4583  cmpt 4643   × cxp 5036  cres 5040   Fn wfn 5799  wf 5800  1-1wf1 5801  ontowfo 5802  1-1-ontowf1o 5803  cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058  𝑚 cmap 7744  Fincfn 7841  cc 9813  cr 9814  0cc0 9815   + caddc 9818  cle 9954  cmin 10145  0cn0 11169  cz 11254  ...cfz 12197  Σcsu 14264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-ico 12052  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265
This theorem is referenced by:  dvnprodlem2  38837
  Copyright terms: Public domain W3C validator