Metamath Proof Explorer

Theorem chnccat

Description: Concatenate two chains. (Contributed by Ender Ting, 20-Jan-2026)

Ref Expression
Hypotheses chnccat.1 ⊢ ( 𝜑 → 𝑇 ∈ ( < Chain 𝐴 ) )
chnccat.2 ⊢ ( 𝜑 → 𝑈 ∈ ( < Chain 𝐴 ) )
chnccat.3 ⊢ ( 𝜑 → ( 𝑇 = ∅ ∨ 𝑈 = ∅ ∨ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) )
Assertion chnccat ( 𝜑 → ( 𝑇 ++ 𝑈 ) ∈ ( < Chain 𝐴 ) )

Proof

Step Hyp Ref Expression
1 chnccat.1 ⊢ ( 𝜑 → 𝑇 ∈ ( < Chain 𝐴 ) )
2 chnccat.2 ⊢ ( 𝜑 → 𝑈 ∈ ( < Chain 𝐴 ) )
3 chnccat.3 ⊢ ( 𝜑 → ( 𝑇 = ∅ ∨ 𝑈 = ∅ ∨ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) )
4 1 chnwrd ⊢ ( 𝜑 → 𝑇 ∈ Word 𝐴 )
5 2 chnwrd ⊢ ( 𝜑 → 𝑈 ∈ Word 𝐴 )
6 ccatcl ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ) → ( 𝑇 ++ 𝑈 ) ∈ Word 𝐴 )
7 4 5 6 syl2anc ⊢ ( 𝜑 → ( 𝑇 ++ 𝑈 ) ∈ Word 𝐴 )
8 eqidd ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) = ( ♯ ‘ 𝑇 ) )
9 8 4 wrdfd ⊢ ( 𝜑 → 𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ 𝐴 )
10 9 fdmd ⊢ ( 𝜑 → dom 𝑇 = ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
11 10 difeq1d ⊢ ( 𝜑 → ( dom 𝑇 ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑛 ∈ ( dom 𝑇 ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ↔ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
13 12 biimpar ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ( dom 𝑇 ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
14 snsspr1 ⊢ { 0 } ⊆ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) }
15 sscon ⊢ ( { 0 } ⊆ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } → ( dom 𝑇 ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ⊆ ( dom 𝑇 ∖ { 0 } ) )
16 14 15 ax-mp ⊢ ( dom 𝑇 ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ⊆ ( dom 𝑇 ∖ { 0 } )
17 16 sseli ⊢ ( 𝑛 ∈ ( dom 𝑇 ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → 𝑛 ∈ ( dom 𝑇 ∖ { 0 } ) )
18 ischn ⊢ ( 𝑇 ∈ ( < Chain 𝐴 ) ↔ ( 𝑇 ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom 𝑇 ∖ { 0 } ) ( 𝑇 ‘ ( 𝑛 − 1 ) ) < ( 𝑇 ‘ 𝑛 ) ) )
19 1 18 sylib ⊢ ( 𝜑 → ( 𝑇 ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom 𝑇 ∖ { 0 } ) ( 𝑇 ‘ ( 𝑛 − 1 ) ) < ( 𝑇 ‘ 𝑛 ) ) )
20 19 simprd ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( dom 𝑇 ∖ { 0 } ) ( 𝑇 ‘ ( 𝑛 − 1 ) ) < ( 𝑇 ‘ 𝑛 ) )
21 20 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom 𝑇 ∖ { 0 } ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) < ( 𝑇 ‘ 𝑛 ) )
22 17 21 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom 𝑇 ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) < ( 𝑇 ‘ 𝑛 ) )
23 13 22 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) < ( 𝑇 ‘ 𝑛 ) )
24 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑇 ∈ Word 𝐴 )
25 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑈 ∈ Word 𝐴 )
26 sscon ⊢ ( { 0 } ⊆ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } → ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ⊆ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 } ) )
27 14 26 ax-mp ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ⊆ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 } )
28 27 sseli ⊢ ( 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 } ) )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 } ) )
30 lencl ⊢ ( 𝑇 ∈ Word 𝐴 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
31 4 30 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
33 29 32 elfzodif0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
34 ccatval1 ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ∧ ( 𝑛 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) = ( 𝑇 ‘ ( 𝑛 − 1 ) ) )
35 24 25 33 34 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) = ( 𝑇 ‘ ( 𝑛 − 1 ) ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
37 36 eldifad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
38 ccatval1 ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
39 24 25 37 38 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
40 23 35 39 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
41 40 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ) ∧ 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑇 = ∅ ) → 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
44 noel ⊢ ¬ 𝑛 ∈ ∅
45 fveq2 ⊢ ( 𝑇 = ∅ → ( ♯ ‘ 𝑇 ) = ( ♯ ‘ ∅ ) )
46 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
47 45 46 eqtrdi ⊢ ( 𝑇 = ∅ → ( ♯ ‘ 𝑇 ) = 0 )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑇 = ∅ ) → ( ♯ ‘ 𝑇 ) = 0 )
49 48 sneqd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑇 = ∅ ) → { ( ♯ ‘ 𝑇 ) } = { 0 } )
50 49 difeq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑇 = ∅ ) → ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ( { 0 } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
51 difpr ⊢ ( { 0 } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ( ( { 0 } ∖ { 0 } ) ∖ { ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
52 difid ⊢ ( { 0 } ∖ { 0 } ) = ∅
53 52 difeq1i ⊢ ( ( { 0 } ∖ { 0 } ) ∖ { ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ( ∅ ∖ { ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
54 0dif ⊢ ( ∅ ∖ { ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ∅
55 51 53 54 3eqtri ⊢ ( { 0 } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ∅
56 50 55 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑇 = ∅ ) → ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ∅ )
57 56 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑇 = ∅ ) → ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ↔ 𝑛 ∈ ∅ ) )
58 44 57 mtbiri ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑇 = ∅ ) → ¬ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
59 43 58 pm2.21dd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑇 = ∅ ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
60 eldifi ⊢ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } )
61 60 elsnd ⊢ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → 𝑛 = ( ♯ ‘ 𝑇 ) )
62 61 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → 𝑛 = ( ♯ ‘ 𝑇 ) )
63 vex ⊢ 𝑛 ∈ V
64 63 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → 𝑛 ∈ V )
65 eldifn ⊢ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
66 65 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
67 fveq2 ⊢ ( 𝑈 = ∅ → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ∅ ) )
68 67 46 eqtrdi ⊢ ( 𝑈 = ∅ → ( ♯ ‘ 𝑈 ) = 0 )
69 68 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → ( ♯ ‘ 𝑈 ) = 0 )
70 69 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) + 0 ) )
71 nn0cn ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℕ0 → ( ♯ ‘ 𝑇 ) ∈ ℂ )
72 4 30 71 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) ∈ ℂ )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑇 ) ∈ ℂ )
74 73 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → ( ♯ ‘ 𝑇 ) ∈ ℂ )
75 74 addridd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → ( ( ♯ ‘ 𝑇 ) + 0 ) = ( ♯ ‘ 𝑇 ) )
76 70 75 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) = ( ♯ ‘ 𝑇 ) )
77 76 preq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } = { 0 , ( ♯ ‘ 𝑇 ) } )
78 66 77 neleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → ¬ 𝑛 ∈ { 0 , ( ♯ ‘ 𝑇 ) } )
79 64 78 nelpr2 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → 𝑛 ≠ ( ♯ ‘ 𝑇 ) )
80 62 79 pm2.21ddne ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑈 = ∅ ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
81 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) )
82 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑇 ∈ Word 𝐴 )
83 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → 𝑇 ∈ Word 𝐴 )
84 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑈 ∈ Word 𝐴 )
85 84 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → 𝑈 ∈ Word 𝐴 )
86 42 eldifad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } )
87 86 elsnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 = ( ♯ ‘ 𝑇 ) )
88 87 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 − 1 ) = ( ( ♯ ‘ 𝑇 ) − 1 ) )
89 82 30 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
90 sscon ⊢ ( { 0 } ⊆ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } → ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ⊆ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 } ) )
91 14 90 ax-mp ⊢ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ⊆ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 } )
92 91 sseli ⊢ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 } ) )
93 61 92 eqeltrrd ⊢ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → ( ♯ ‘ 𝑇 ) ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 } ) )
94 93 eldifbd ⊢ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → ¬ ( ♯ ‘ 𝑇 ) ∈ { 0 } )
95 94 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ¬ ( ♯ ‘ 𝑇 ) ∈ { 0 } )
96 89 95 eldifd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑇 ) ∈ ( ℕ0 ∖ { 0 } ) )
97 dfn2 ⊢ ℕ = ( ℕ0 ∖ { 0 } )
98 96 97 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑇 ) ∈ ℕ )
99 fzo0end ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℕ → ( ( ♯ ‘ 𝑇 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
100 98 99 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( ♯ ‘ 𝑇 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
101 88 100 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
102 101 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( 𝑛 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
103 83 85 102 34 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) = ( 𝑇 ‘ ( 𝑛 − 1 ) ) )
104 61 oveq1d ⊢ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → ( 𝑛 − 1 ) = ( ( ♯ ‘ 𝑇 ) − 1 ) )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 − 1 ) = ( ( ♯ ‘ 𝑇 ) − 1 ) )
106 105 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = ( 𝑇 ‘ ( ( ♯ ‘ 𝑇 ) − 1 ) ) )
107 lsw ⊢ ( 𝑇 ∈ Word 𝐴 → ( lastS ‘ 𝑇 ) = ( 𝑇 ‘ ( ( ♯ ‘ 𝑇 ) − 1 ) ) )
108 82 107 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( lastS ‘ 𝑇 ) = ( 𝑇 ‘ ( ( ♯ ‘ 𝑇 ) − 1 ) ) )
109 106 108 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = ( lastS ‘ 𝑇 ) )
110 109 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( 𝑇 ‘ ( 𝑛 − 1 ) ) = ( lastS ‘ 𝑇 ) )
111 103 110 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) = ( lastS ‘ 𝑇 ) )
112 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → 𝑛 = ( ♯ ‘ 𝑇 ) )
113 112 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( ♯ ‘ 𝑇 ) ) )
114 lencl ⊢ ( 𝑈 ∈ Word 𝐴 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
115 5 114 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
116 115 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
117 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( ♯ ‘ 𝑈 ) = 0 ) → 𝑇 ∈ Word 𝐴 )
118 117 30 71 3syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ♯ ‘ 𝑇 ) ∈ ℂ )
119 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ♯ ‘ 𝑈 ) = 0 )
120 118 119 jca ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) )
121 prid2g ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℂ → ( ♯ ‘ 𝑇 ) ∈ { 0 , ( ♯ ‘ 𝑇 ) } )
122 121 adantr ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ♯ ‘ 𝑇 ) ∈ { 0 , ( ♯ ‘ 𝑇 ) } )
123 simpr ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ♯ ‘ 𝑈 ) = 0 )
124 123 oveq2d ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) + 0 ) )
125 addrid ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℂ → ( ( ♯ ‘ 𝑇 ) + 0 ) = ( ♯ ‘ 𝑇 ) )
126 125 adantr ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ( ♯ ‘ 𝑇 ) + 0 ) = ( ♯ ‘ 𝑇 ) )
127 124 126 eqtrd ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) = ( ♯ ‘ 𝑇 ) )
128 127 preq2d ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } = { 0 , ( ♯ ‘ 𝑇 ) } )
129 122 128 eleqtrrd ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( ♯ ‘ 𝑇 ) ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
130 129 snssd ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → { ( ♯ ‘ 𝑇 ) } ⊆ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
131 ssdif0 ⊢ ( { ( ♯ ‘ 𝑇 ) } ⊆ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ↔ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ∅ )
132 130 131 sylib ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ∅ )
133 nel02 ⊢ ( ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ∅ → ¬ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
134 120 132 133 3syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( ♯ ‘ 𝑈 ) = 0 ) → ¬ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
135 134 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( ♯ ‘ 𝑈 ) = 0 → ¬ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
136 42 135 mt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ¬ ( ♯ ‘ 𝑈 ) = 0 )
137 136 neqned ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑈 ) ≠ 0 )
138 elnnne0 ⊢ ( ( ♯ ‘ 𝑈 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑈 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑈 ) ≠ 0 ) )
139 116 137 138 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑈 ) ∈ ℕ )
140 139 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( ♯ ‘ 𝑈 ) ∈ ℕ )
141 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ↔ ( ♯ ‘ 𝑈 ) ∈ ℕ )
142 140 141 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
143 addlid ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℂ → ( 0 + ( ♯ ‘ 𝑇 ) ) = ( ♯ ‘ 𝑇 ) )
144 143 eqcomd ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℂ → ( ♯ ‘ 𝑇 ) = ( 0 + ( ♯ ‘ 𝑇 ) ) )
145 144 fveq2d ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℂ → ( ( 𝑇 ++ 𝑈 ) ‘ ( ♯ ‘ 𝑇 ) ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( 0 + ( ♯ ‘ 𝑇 ) ) ) )
146 30 71 145 3syl ⊢ ( 𝑇 ∈ Word 𝐴 → ( ( 𝑇 ++ 𝑈 ) ‘ ( ♯ ‘ 𝑇 ) ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( 0 + ( ♯ ‘ 𝑇 ) ) ) )
147 146 3ad2ant1 ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( ♯ ‘ 𝑇 ) ) = ( ( 𝑇 ++ 𝑈 ) ‘ ( 0 + ( ♯ ‘ 𝑇 ) ) ) )
148 ccatval3 ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 0 + ( ♯ ‘ 𝑇 ) ) ) = ( 𝑈 ‘ 0 ) )
149 147 148 eqtrd ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( ♯ ‘ 𝑇 ) ) = ( 𝑈 ‘ 0 ) )
150 83 85 142 149 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( ♯ ‘ 𝑇 ) ) = ( 𝑈 ‘ 0 ) )
151 113 150 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) = ( 𝑈 ‘ 0 ) )
152 81 111 151 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
153 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑇 = ∅ ∨ 𝑈 = ∅ ∨ ( lastS ‘ 𝑇 ) < ( 𝑈 ‘ 0 ) ) )
154 59 80 152 153 mpjao3dan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
155 154 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ) ∧ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
156 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
157 eldifi ⊢ ( 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) )
158 157 eldifad ⊢ ( 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
159 elfzoelz ⊢ ( 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) → 𝑛 ∈ ℤ )
160 158 159 syl ⊢ ( 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) → 𝑛 ∈ ℤ )
161 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
162 156 160 161 3syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ℂ )
163 1cnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 1 ∈ ℂ )
164 72 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑇 ) ∈ ℂ )
165 162 163 164 sub32d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑛 − 1 ) − ( ♯ ‘ 𝑇 ) ) = ( ( 𝑛 − ( ♯ ‘ 𝑇 ) ) − 1 ) )
166 165 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑈 ‘ ( ( 𝑛 − 1 ) − ( ♯ ‘ 𝑇 ) ) ) = ( 𝑈 ‘ ( ( 𝑛 − ( ♯ ‘ 𝑇 ) ) − 1 ) ) )
167 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑈 ∈ ( < Chain 𝐴 ) )
168 158 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
169 nn0z ⊢ ( ( ♯ ‘ 𝑈 ) ∈ ℕ0 → ( ♯ ‘ 𝑈 ) ∈ ℤ )
170 5 114 169 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℤ )
171 170 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ♯ ‘ 𝑈 ) ∈ ℤ )
172 fzosubel3 ⊢ ( ( 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ( ♯ ‘ 𝑈 ) ∈ ℤ ) → ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
173 168 171 172 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
174 simpl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝜑 )
175 156 eldifad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) )
176 174 175 jca ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) )
177 eldifi ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) → 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
178 177 159 161 3syl ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) → 𝑛 ∈ ℂ )
179 178 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → 𝑛 ∈ ℂ )
180 72 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( ♯ ‘ 𝑇 ) ∈ ℂ )
181 eldifsni ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) → 𝑛 ≠ ( ♯ ‘ 𝑇 ) )
182 181 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → 𝑛 ≠ ( ♯ ‘ 𝑇 ) )
183 179 180 182 subne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ≠ 0 )
184 nelsn ⊢ ( ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ≠ 0 → ¬ ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ { 0 } )
185 176 183 184 3syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ¬ ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ { 0 } )
186 173 185 eldifd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ∖ { 0 } ) )
187 eqidd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑈 ) )
188 187 5 wrdfd ⊢ ( 𝜑 → 𝑈 : ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ⟶ 𝐴 )
189 188 fdmd ⊢ ( 𝜑 → dom 𝑈 = ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
190 189 difeq1d ⊢ ( 𝜑 → ( dom 𝑈 ∖ { 0 } ) = ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ∖ { 0 } ) )
191 190 eleq2d ⊢ ( 𝜑 → ( ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ ( dom 𝑈 ∖ { 0 } ) ↔ ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ∖ { 0 } ) ) )
192 191 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ ( ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ∖ { 0 } ) ) → ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ ( dom 𝑈 ∖ { 0 } ) )
193 186 192 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ∈ ( dom 𝑈 ∖ { 0 } ) )
194 167 193 chnltm1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑈 ‘ ( ( 𝑛 − ( ♯ ‘ 𝑇 ) ) − 1 ) ) < ( 𝑈 ‘ ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ) )
195 166 194 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑈 ‘ ( ( 𝑛 − 1 ) − ( ♯ ‘ 𝑇 ) ) ) < ( 𝑈 ‘ ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ) )
196 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑇 ∈ Word 𝐴 )
197 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → 𝑈 ∈ Word 𝐴 )
198 177 159 syl ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) → 𝑛 ∈ ℤ )
199 198 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → 𝑛 ∈ ℤ )
200 nn0z ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℕ0 → ( ♯ ‘ 𝑇 ) ∈ ℤ )
201 4 30 200 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) ∈ ℤ )
202 201 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( ♯ ‘ 𝑇 ) ∈ ℤ )
203 199 202 jca ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) )
204 elfzole1 ⊢ ( 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) → ( ♯ ‘ 𝑇 ) ≤ 𝑛 )
205 177 204 syl ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) → ( ♯ ‘ 𝑇 ) ≤ 𝑛 )
206 205 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( ♯ ‘ 𝑇 ) ≤ 𝑛 )
207 eldifn ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) → ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } )
208 velsn ⊢ ( 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ↔ 𝑛 = ( ♯ ‘ 𝑇 ) )
209 208 biimpri ⊢ ( 𝑛 = ( ♯ ‘ 𝑇 ) → 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } )
210 209 necon3bi ⊢ ( ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → 𝑛 ≠ ( ♯ ‘ 𝑇 ) )
211 210 necomd ⊢ ( ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → ( ♯ ‘ 𝑇 ) ≠ 𝑛 )
212 207 211 syl ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) → ( ♯ ‘ 𝑇 ) ≠ 𝑛 )
213 212 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( ♯ ‘ 𝑇 ) ≠ 𝑛 )
214 simp1r ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ♯ ‘ 𝑇 ) ∈ ℤ )
215 214 zred ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ♯ ‘ 𝑇 ) ∈ ℝ )
216 simp1l ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → 𝑛 ∈ ℤ )
217 216 zred ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → 𝑛 ∈ ℝ )
218 simp2 ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ♯ ‘ 𝑇 ) ≤ 𝑛 )
219 simp3 ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ♯ ‘ 𝑇 ) ≠ 𝑛 )
220 219 necomd ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → 𝑛 ≠ ( ♯ ‘ 𝑇 ) )
221 215 217 218 220 leneltd ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ♯ ‘ 𝑇 ) < 𝑛 )
222 simp1 ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) )
223 222 ancomd ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ( ♯ ‘ 𝑇 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
224 zltp1le ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ♯ ‘ 𝑇 ) < 𝑛 ↔ ( ( ♯ ‘ 𝑇 ) + 1 ) ≤ 𝑛 ) )
225 223 224 syl ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ( ♯ ‘ 𝑇 ) < 𝑛 ↔ ( ( ♯ ‘ 𝑇 ) + 1 ) ≤ 𝑛 ) )
226 221 225 mpbid ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ( ♯ ‘ 𝑇 ) + 1 ) ≤ 𝑛 )
227 peano2re ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℝ → ( ( ♯ ‘ 𝑇 ) + 1 ) ∈ ℝ )
228 215 227 syl ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ( ♯ ‘ 𝑇 ) + 1 ) ∈ ℝ )
229 1red ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → 1 ∈ ℝ )
230 228 217 229 lesub1d ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ( ( ♯ ‘ 𝑇 ) + 1 ) ≤ 𝑛 ↔ ( ( ( ♯ ‘ 𝑇 ) + 1 ) − 1 ) ≤ ( 𝑛 − 1 ) ) )
231 zcn ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℤ → ( ♯ ‘ 𝑇 ) ∈ ℂ )
232 1cnd ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℤ → 1 ∈ ℂ )
233 231 232 pncand ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℤ → ( ( ( ♯ ‘ 𝑇 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑇 ) )
234 233 adantl ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) → ( ( ( ♯ ‘ 𝑇 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑇 ) )
235 234 3ad2ant1 ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ( ( ♯ ‘ 𝑇 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑇 ) )
236 235 breq1d ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ( ( ( ♯ ‘ 𝑇 ) + 1 ) − 1 ) ≤ ( 𝑛 − 1 ) ↔ ( ♯ ‘ 𝑇 ) ≤ ( 𝑛 − 1 ) ) )
237 230 236 bitrd ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ( ( ♯ ‘ 𝑇 ) + 1 ) ≤ 𝑛 ↔ ( ♯ ‘ 𝑇 ) ≤ ( 𝑛 − 1 ) ) )
238 226 237 mpbid ⊢ ( ( ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) ∧ ( ♯ ‘ 𝑇 ) ≤ 𝑛 ∧ ( ♯ ‘ 𝑇 ) ≠ 𝑛 ) → ( ♯ ‘ 𝑇 ) ≤ ( 𝑛 − 1 ) )
239 203 206 213 238 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( ♯ ‘ 𝑇 ) ≤ ( 𝑛 − 1 ) )
240 199 zred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → 𝑛 ∈ ℝ )
241 peano2rem ⊢ ( 𝑛 ∈ ℝ → ( 𝑛 − 1 ) ∈ ℝ )
242 240 241 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( 𝑛 − 1 ) ∈ ℝ )
243 201 170 zaddcld ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ℤ )
244 243 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ℤ )
245 244 zred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ℝ )
246 240 ltm1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( 𝑛 − 1 ) < 𝑛 )
247 elfzolt2 ⊢ ( 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) → 𝑛 < ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
248 177 247 syl ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) → 𝑛 < ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
249 248 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → 𝑛 < ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
250 242 240 245 246 249 lttrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( 𝑛 − 1 ) < ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
251 peano2zm ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 − 1 ) ∈ ℤ )
252 199 251 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( 𝑛 − 1 ) ∈ ℤ )
253 elfzo ⊢ ( ( ( 𝑛 − 1 ) ∈ ℤ ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ℤ ) → ( ( 𝑛 − 1 ) ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ↔ ( ( ♯ ‘ 𝑇 ) ≤ ( 𝑛 − 1 ) ∧ ( 𝑛 − 1 ) < ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) )
254 252 202 244 253 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( ( 𝑛 − 1 ) ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ↔ ( ( ♯ ‘ 𝑇 ) ≤ ( 𝑛 − 1 ) ∧ ( 𝑛 − 1 ) < ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) )
255 239 250 254 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) → ( 𝑛 − 1 ) ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
256 157 255 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 − 1 ) ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
257 ccatval2 ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ∧ ( 𝑛 − 1 ) ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) = ( 𝑈 ‘ ( ( 𝑛 − 1 ) − ( ♯ ‘ 𝑇 ) ) ) )
258 196 197 256 257 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) = ( 𝑈 ‘ ( ( 𝑛 − 1 ) − ( ♯ ‘ 𝑇 ) ) ) )
259 ccatval2 ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) = ( 𝑈 ‘ ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ) )
260 196 197 168 259 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) = ( 𝑈 ‘ ( 𝑛 − ( ♯ ‘ 𝑇 ) ) ) )
261 195 258 260 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
262 261 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ) ∧ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
263 ccatlen ⊢ ( ( 𝑇 ∈ Word 𝐴 ∧ 𝑈 ∈ Word 𝐴 ) → ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
264 4 5 263 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
265 264 eqcomd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) = ( ♯ ‘ ( 𝑇 ++ 𝑈 ) ) )
266 265 7 wrdfd ⊢ ( 𝜑 → ( 𝑇 ++ 𝑈 ) : ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ⟶ 𝐴 )
267 266 fdmd ⊢ ( 𝜑 → dom ( 𝑇 ++ 𝑈 ) = ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
268 267 difeq1d ⊢ ( 𝜑 → ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) )
269 fzonel ⊢ ¬ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) )
270 simpr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) )
271 270 eldifad ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
272 271 ex ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) → ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) )
273 269 272 mtoi ⊢ ( 𝜑 → ¬ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) )
274 difsn ⊢ ( ¬ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) → ( ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) ∖ { ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) )
275 274 eqcomd ⊢ ( ¬ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) → ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) = ( ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) ∖ { ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
276 273 275 syl ⊢ ( 𝜑 → ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) = ( ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) ∖ { ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
277 difpr ⊢ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) = ( ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) ∖ { ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
278 276 277 eqtr4di ⊢ ( 𝜑 → ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 } ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
279 268 278 eqtrd ⊢ ( 𝜑 → ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
280 279 eleq2d ⊢ ( 𝜑 → ( 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ↔ 𝑛 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
281 eldif ⊢ ( 𝑛 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ↔ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
282 280 281 bitrdi ⊢ ( 𝜑 → ( 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ↔ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
283 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
284 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
285 283 284 eldifd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
286 285 orcd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ) )
287 exmidd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ∨ ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ) )
288 idd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ) )
289 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } )
290 288 289 jctird ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → ( 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
291 eldif ⊢ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ↔ ( 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
292 290 291 imbitrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
293 idd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ) )
294 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) )
295 293 294 jctild ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → ( 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ) ) )
296 eldif ⊢ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ↔ ( 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ) )
297 295 296 imbitrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ) )
298 297 289 jctird ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
299 eldif ⊢ ( 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ↔ ( 𝑛 ∈ ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) )
300 298 299 imbitrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } → 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
301 292 300 orim12d ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( ( 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ∨ ¬ 𝑛 ∈ { ( ♯ ‘ 𝑇 ) } ) → ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ) )
302 287 301 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
303 302 olcd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ∧ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ) )
304 201 anim1ci ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) → ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) )
305 304 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) )
306 fzospliti ⊢ ( ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) → ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∨ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) )
307 305 306 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∨ 𝑛 ∈ ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ) )
308 286 303 307 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∧ ¬ 𝑛 ∈ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) → ( 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ) )
309 282 308 sylbida ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ) → ( 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ) )
310 3orass ⊢ ( ( 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ↔ ( 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ ( 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) ) )
311 309 310 sylibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ) → ( 𝑛 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( { ( ♯ ‘ 𝑇 ) } ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ∨ 𝑛 ∈ ( ( ( ( ♯ ‘ 𝑇 ) ..^ ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) ) ∖ { ( ♯ ‘ 𝑇 ) } ) ∖ { 0 , ( ( ♯ ‘ 𝑇 ) + ( ♯ ‘ 𝑈 ) ) } ) ) )
312 41 155 262 311 mpjao3dan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ) → ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
313 312 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) )
314 ischn ⊢ ( ( 𝑇 ++ 𝑈 ) ∈ ( < Chain 𝐴 ) ↔ ( ( 𝑇 ++ 𝑈 ) ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom ( 𝑇 ++ 𝑈 ) ∖ { 0 } ) ( ( 𝑇 ++ 𝑈 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝑇 ++ 𝑈 ) ‘ 𝑛 ) ) )
315 7 313 314 sylanbrc ⊢ ( 𝜑 → ( 𝑇 ++ 𝑈 ) ∈ ( < Chain 𝐴 ) )