Metamath Proof Explorer

Theorem chnccat

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

Ref Expression
Hypotheses chnccat.1 
|- ( ph -> T e. ( .< Chain A ) )
chnccat.2 
|- ( ph -> U e. ( .< Chain A ) )
chnccat.3 
|- ( ph -> ( T = (/) \/ U = (/) \/ ( lastS ` T ) .< ( U ` 0 ) ) )
Assertion chnccat 
|- ( ph -> ( T ++ U ) e. ( .< Chain A ) )

Proof

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