This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ccatws1f1o

Description: Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses ccatws1f1o.1 ⊢ 𝑁 = ( ♯ ‘ 𝑇 )
ccatws1f1o.2 ⊢ 𝐽 = ( 0 ..^ ( 𝑁 + 1 ) )
ccatws1f1o.3 ⊢ ( 𝜑 → 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
Assertion ccatws1f1o ( 𝜑 → ( 𝑇 ++ ⟨“ 𝑁 ”⟩ ) : 𝐽 –1-1-onto→ 𝐽 )

Proof

Step Hyp Ref Expression
1 ccatws1f1o.1 ⊢ 𝑁 = ( ♯ ‘ 𝑇 )
2 ccatws1f1o.2 ⊢ 𝐽 = ( 0 ..^ ( 𝑁 + 1 ) )
3 ccatws1f1o.3 ⊢ ( 𝜑 → 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
4 f1of ⊢ ( 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) → 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) )
5 3 4 syl ⊢ ( 𝜑 → 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) )
6 iswrdi ⊢ ( 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) → 𝑇 ∈ Word ( 0 ..^ 𝑁 ) )
7 lencl ⊢ ( 𝑇 ∈ Word ( 0 ..^ 𝑁 ) → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
8 5 6 7 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
9 1 8 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
10 fzossfzop1 ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )
11 9 10 syl ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )
12 11 2 sseqtrrdi ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ 𝐽 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 0 ..^ 𝑁 ) ⊆ 𝐽 )
14 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) )
15 1 eqcomi ⊢ ( ♯ ‘ 𝑇 ) = 𝑁
16 15 a1i ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) = 𝑁 )
17 16 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑇 ) ) = ( 0 ..^ 𝑁 ) )
18 17 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) )
19 18 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑥 ∈ ( 0 ..^ 𝑁 ) )
20 14 19 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑇 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
21 13 20 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝐽 )
22 21 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝐽 )
23 2 a1i ⊢ ( 𝜑 → 𝐽 = ( 0 ..^ ( 𝑁 + 1 ) ) )
24 fzo0ssnn0 ⊢ ( 0 ..^ ( 𝑁 + 1 ) ) ⊆ ℕ0
25 23 24 eqsstrdi ⊢ ( 𝜑 → 𝐽 ⊆ ℕ0 )
26 25 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ℕ0 )
27 26 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ℂ )
28 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑥 ∈ ℂ )
29 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
30 9 29 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
31 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
32 23 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐽 ↔ 𝑥 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
33 32 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑥 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
35 fzosplitsni ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑥 = 𝑁 ) ) )
36 35 biimpa ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑥 = 𝑁 ) )
37 31 34 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑥 = 𝑁 ) )
38 18 notbid ⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ ¬ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) )
39 38 biimpa ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ¬ 𝑥 ∈ ( 0 ..^ 𝑁 ) )
40 39 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ¬ 𝑥 ∈ ( 0 ..^ 𝑁 ) )
41 37 40 orcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑥 = 𝑁 )
42 41 1 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑥 = ( ♯ ‘ 𝑇 ) )
43 28 42 subeq0bd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑇 ) ) = 0 )
44 43 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) = ( ⟨“ 𝑁 ”⟩ ‘ 0 ) )
45 s1fv ⊢ ( 𝑁 ∈ ℕ0 → ( ⟨“ 𝑁 ”⟩ ‘ 0 ) = 𝑁 )
46 9 45 syl ⊢ ( 𝜑 → ( ⟨“ 𝑁 ”⟩ ‘ 0 ) = 𝑁 )
47 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ⟨“ 𝑁 ”⟩ ‘ 0 ) = 𝑁 )
48 44 47 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) = 𝑁 )
49 fzonn0p1 ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
50 9 49 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
51 50 2 eleqtrrdi ⊢ ( 𝜑 → 𝑁 ∈ 𝐽 )
52 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑁 ∈ 𝐽 )
53 48 52 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ∈ 𝐽 )
54 22 53 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ∈ 𝐽 )
55 54 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐽 if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ∈ 𝐽 )
56 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ 𝑁 ) ⊆ 𝐽 )
57 f1ocnv ⊢ ( 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) → ◡ 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
58 f1of ⊢ ( ◡ 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) → ◡ 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) )
59 3 57 58 3syl ⊢ ( 𝜑 → ◡ 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ◡ 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) )
61 60 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ◡ 𝑇 ‘ 𝑦 ) ∈ ( 0 ..^ 𝑁 ) )
62 56 61 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ◡ 𝑇 ‘ 𝑦 ) ∈ 𝐽 )
63 1 oveq2i ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝑇 ) )
64 61 63 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ◡ 𝑇 ‘ 𝑦 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
65 64 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( ◡ 𝑇 ‘ 𝑦 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) , ( ⟨“ 𝑁 ”⟩ ‘ ( ( ◡ 𝑇 ‘ 𝑦 ) − ( ♯ ‘ 𝑇 ) ) ) ) = ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) )
66 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
67 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
68 f1ocnvfv2 ⊢ ( ( 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) = 𝑦 )
69 66 67 68 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) = 𝑦 )
70 65 69 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 = if ( ( ◡ 𝑇 ‘ 𝑦 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) , ( ⟨“ 𝑁 ”⟩ ‘ ( ( ◡ 𝑇 ‘ 𝑦 ) − ( ♯ ‘ 𝑇 ) ) ) ) )
71 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
72 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
73 72 33 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑥 = 𝑁 ) )
74 73 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑥 = 𝑁 ) )
75 67 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
76 71 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
77 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → 𝑥 = 𝑁 )
78 fzonel ⊢ ¬ 𝑁 ∈ ( 0 ..^ 𝑁 )
79 78 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → ¬ 𝑁 ∈ ( 0 ..^ 𝑁 ) )
80 63 eleq2i ⊢ ( 𝑁 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
81 79 80 sylnib ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
82 77 81 eqneltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
83 82 iffalsed ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) = ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) )
84 2 24 eqsstri ⊢ 𝐽 ⊆ ℕ0
85 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → 𝑥 ∈ 𝐽 )
86 84 85 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → 𝑥 ∈ ℕ0 )
87 86 nn0cnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → 𝑥 ∈ ℂ )
88 77 1 eqtrdi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → 𝑥 = ( ♯ ‘ 𝑇 ) )
89 87 88 subeq0bd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → ( 𝑥 − ( ♯ ‘ 𝑇 ) ) = 0 )
90 89 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) = ( ⟨“ 𝑁 ”⟩ ‘ 0 ) )
91 46 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → ( ⟨“ 𝑁 ”⟩ ‘ 0 ) = 𝑁 )
92 90 91 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) = 𝑁 )
93 76 83 92 3eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → 𝑦 = 𝑁 )
94 93 79 eqneltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 = 𝑁 ) → ¬ 𝑦 ∈ ( 0 ..^ 𝑁 ) )
95 75 94 pm2.65da ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → ¬ 𝑥 = 𝑁 )
96 74 95 olcnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑥 ∈ ( 0 ..^ 𝑁 ) )
97 96 63 eleqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
98 97 iftrued ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) = ( 𝑇 ‘ 𝑥 ) )
99 71 98 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑦 = ( 𝑇 ‘ 𝑥 ) )
100 99 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → ( ◡ 𝑇 ‘ 𝑦 ) = ( ◡ 𝑇 ‘ ( 𝑇 ‘ 𝑥 ) ) )
101 66 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
102 f1ocnvfv1 ⊢ ( ( 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ◡ 𝑇 ‘ ( 𝑇 ‘ 𝑥 ) ) = 𝑥 )
103 101 96 102 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → ( ◡ 𝑇 ‘ ( 𝑇 ‘ 𝑥 ) ) = 𝑥 )
104 100 103 eqtr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) )
105 104 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) ) )
106 105 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ 𝐽 ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) ) )
107 eleq1 ⊢ ( 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ ( ◡ 𝑇 ‘ 𝑦 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) )
108 fveq2 ⊢ ( 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) )
109 fvoveq1 ⊢ ( 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) = ( ⟨“ 𝑁 ”⟩ ‘ ( ( ◡ 𝑇 ‘ 𝑦 ) − ( ♯ ‘ 𝑇 ) ) ) )
110 107 108 109 ifbieq12d ⊢ ( 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) = if ( ( ◡ 𝑇 ‘ 𝑦 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) , ( ⟨“ 𝑁 ”⟩ ‘ ( ( ◡ 𝑇 ‘ 𝑦 ) − ( ♯ ‘ 𝑇 ) ) ) ) )
111 110 eqeq2d ⊢ ( 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) → ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ↔ 𝑦 = if ( ( ◡ 𝑇 ‘ 𝑦 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) , ( ⟨“ 𝑁 ”⟩ ‘ ( ( ◡ 𝑇 ‘ 𝑦 ) − ( ♯ ‘ 𝑇 ) ) ) ) ) )
112 111 eqreu ⊢ ( ( ( ◡ 𝑇 ‘ 𝑦 ) ∈ 𝐽 ∧ 𝑦 = if ( ( ◡ 𝑇 ‘ 𝑦 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ ( ◡ 𝑇 ‘ 𝑦 ) ) , ( ⟨“ 𝑁 ”⟩ ‘ ( ( ◡ 𝑇 ‘ 𝑦 ) − ( ♯ ‘ 𝑇 ) ) ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 = ( ◡ 𝑇 ‘ 𝑦 ) ) ) → ∃! 𝑥 ∈ 𝐽 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
113 62 70 106 112 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ∃! 𝑥 ∈ 𝐽 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
114 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → 𝑁 ∈ 𝐽 )
115 9 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
116 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → 𝑁 ∈ ℂ )
117 1 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → 𝑁 = ( ♯ ‘ 𝑇 ) )
118 116 117 subeq0bd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → ( 𝑁 − ( ♯ ‘ 𝑇 ) ) = 0 )
119 118 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) = ( ⟨“ 𝑁 ”⟩ ‘ 0 ) )
120 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → ( ⟨“ 𝑁 ”⟩ ‘ 0 ) = 𝑁 )
121 119 120 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) = 𝑁 )
122 78 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → ¬ 𝑁 ∈ ( 0 ..^ 𝑁 ) )
123 122 80 sylnib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
124 123 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → if ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑁 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) ) = ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) )
125 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → 𝑦 = 𝑁 )
126 121 124 125 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → 𝑦 = if ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑁 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) ) )
127 30 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
128 127 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
129 33 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑥 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
130 128 129 36 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑥 = 𝑁 ) )
131 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
132 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑦 = 𝑁 )
133 131 132 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) = 𝑁 )
134 133 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) = 𝑁 )
135 63 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
136 135 eleq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) )
137 136 biimpa ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
138 137 iftrued ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) = ( 𝑇 ‘ 𝑥 ) )
139 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) )
140 139 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑇 ‘ 𝑥 ) ∈ ( 0 ..^ 𝑁 ) )
141 138 140 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ∈ ( 0 ..^ 𝑁 ) )
142 134 141 eqeltrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ( 0 ..^ 𝑁 ) )
143 78 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ¬ 𝑁 ∈ ( 0 ..^ 𝑁 ) )
144 142 143 pm2.65da ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → ¬ 𝑥 ∈ ( 0 ..^ 𝑁 ) )
145 130 144 orcnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) → 𝑥 = 𝑁 )
146 145 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 = 𝑁 ) )
147 146 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → ∀ 𝑥 ∈ 𝐽 ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 = 𝑁 ) )
148 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) )
149 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑁 ) )
150 fvoveq1 ⊢ ( 𝑥 = 𝑁 → ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) = ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) )
151 148 149 150 ifbieq12d ⊢ ( 𝑥 = 𝑁 → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) = if ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑁 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) ) )
152 151 eqeq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ↔ 𝑦 = if ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑁 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) ) ) )
153 152 eqreu ⊢ ( ( 𝑁 ∈ 𝐽 ∧ 𝑦 = if ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑁 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑁 − ( ♯ ‘ 𝑇 ) ) ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 = 𝑁 ) ) → ∃! 𝑥 ∈ 𝐽 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
154 114 126 147 153 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑦 = 𝑁 ) → ∃! 𝑥 ∈ 𝐽 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
155 23 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↔ 𝑦 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
156 155 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
157 fzosplitsni ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑦 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑦 = 𝑁 ) ) )
158 157 biimpa ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑦 = 𝑁 ) )
159 127 156 158 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ∨ 𝑦 = 𝑁 ) )
160 113 154 159 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ∃! 𝑥 ∈ 𝐽 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
161 160 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐽 ∃! 𝑥 ∈ 𝐽 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
162 s1len ⊢ ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) = 1
163 15 162 oveq12i ⊢ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) = ( 𝑁 + 1 )
164 163 oveq2i ⊢ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) ) = ( 0 ..^ ( 𝑁 + 1 ) )
165 164 2 eqtr4i ⊢ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) ) = 𝐽
166 165 mpteq1i ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) = ( 𝑥 ∈ 𝐽 ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) )
167 166 f1ompt ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) : 𝐽 –1-1-onto→ 𝐽 ↔ ( ∀ 𝑥 ∈ 𝐽 if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ∈ 𝐽 ∧ ∀ 𝑦 ∈ 𝐽 ∃! 𝑥 ∈ 𝐽 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) )
168 55 161 167 sylanbrc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) : 𝐽 –1-1-onto→ 𝐽 )
169 ovex ⊢ ( 0 ..^ 𝑁 ) ∈ V
170 fex ⊢ ( ( 𝑇 : ( 0 ..^ 𝑁 ) ⟶ ( 0 ..^ 𝑁 ) ∧ ( 0 ..^ 𝑁 ) ∈ V ) → 𝑇 ∈ V )
171 5 169 170 sylancl ⊢ ( 𝜑 → 𝑇 ∈ V )
172 s1cli ⊢ ⟨“ 𝑁 ”⟩ ∈ Word V
173 ccatfval ⊢ ( ( 𝑇 ∈ V ∧ ⟨“ 𝑁 ”⟩ ∈ Word V ) → ( 𝑇 ++ ⟨“ 𝑁 ”⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) )
174 171 172 173 sylancl ⊢ ( 𝜑 → ( 𝑇 ++ ⟨“ 𝑁 ”⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) )
175 174 f1oeq1d ⊢ ( 𝜑 → ( ( 𝑇 ++ ⟨“ 𝑁 ”⟩ ) : 𝐽 –1-1-onto→ 𝐽 ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ ⟨“ 𝑁 ”⟩ ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) , ( 𝑇 ‘ 𝑥 ) , ( ⟨“ 𝑁 ”⟩ ‘ ( 𝑥 − ( ♯ ‘ 𝑇 ) ) ) ) ) : 𝐽 –1-1-onto→ 𝐽 ) )
176 168 175 mpbird ⊢ ( 𝜑 → ( 𝑇 ++ ⟨“ 𝑁 ”⟩ ) : 𝐽 –1-1-onto→ 𝐽 )