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