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