Metamath Proof Explorer

Theorem dvnprodlem1

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

Ref Expression
Hypotheses dvnprodlem1.c ⊢ 𝐶 = ( 𝑠 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡 ∈ 𝑠 ( 𝑐 ‘ 𝑡 ) = 𝑛 } ) )
dvnprodlem1.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
dvnprodlem1.d ⊢ 𝐷 = ( 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ↦ ⟨ ( 𝐽 − ( 𝑐 ‘ 𝑍 ) ) , ( 𝑐 ↾ 𝑅 ) ⟩ )
dvnprodlem1.t ⊢ ( 𝜑 → 𝑇 ∈ Fin )
dvnprodlem1.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
dvnprodlem1.zr ⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝑅 )
dvnprodlem1.rzt ⊢ ( 𝜑 → ( 𝑅 ∪ { 𝑍 } ) ⊆ 𝑇 )
Assertion dvnprodlem1 ( 𝜑 → 𝐷 : ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) –1-1-onto→ ∪ 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶 ‘ 𝑅 ) ‘ 𝑘 ) ) )

Proof

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