Metamath Proof Explorer

Theorem tworepnotupword

Description: Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024)

Ref Expression
Hypothesis tworepnotupword.1 
|- A e. _V
Assertion tworepnotupword 
|- -. ( <" A "> ++ <" A "> ) e. UpWord S

Proof

Step Hyp Ref Expression
1 tworepnotupword.1 
 |-  A e. _V
2 ovex 
 |-  ( <" A "> ++ <" A "> ) e. _V
3 c0ex 
 |-  0 e. _V
4 3 isseti 
 |-  E. k k = 0
5 0z 
 |-  0 e. ZZ
6 ccat2s1len 
 |-  ( # ` ( <" A "> ++ <" A "> ) ) = 2
7 6 oveq1i 
 |-  ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) = ( 2 - 1 )
8 2m1e1 
 |-  ( 2 - 1 ) = 1
9 7 8 eqtri 
 |-  ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) = 1
10 1z 
 |-  1 e. ZZ
11 9 10 eqeltri 
 |-  ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) e. ZZ
12 0lt1 
 |-  0 < 1
13 12 9 breqtrri 
 |-  0 < ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 )
14 fzolb 
 |-  ( 0 e. ( 0 ..^ ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) ) <-> ( 0 e. ZZ /\ ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) e. ZZ /\ 0 < ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) ) )
15 5 11 13 14 mpbir3an 
 |-  0 e. ( 0 ..^ ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) )
16 eleq1a 
 |-  ( 0 e. ( 0 ..^ ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) ) -> ( k = 0 -> k e. ( 0 ..^ ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) ) ) )
17 15 16 ax-mp 
 |-  ( k = 0 -> k e. ( 0 ..^ ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) ) )
18 fveq2 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( # ` b ) = ( # ` ( <" A "> ++ <" A "> ) ) )
19 18 oveq1d 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( ( # ` b ) - 1 ) = ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) )
20 19 oveq2d 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( 0 ..^ ( ( # ` b ) - 1 ) ) = ( 0 ..^ ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) ) )
21 20 eleq2d 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) <-> k e. ( 0 ..^ ( ( # ` ( <" A "> ++ <" A "> ) ) - 1 ) ) ) )
22 17 21 imbitrrid 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( k = 0 -> k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ) )
23 et-ltneverrefl 
 |-  -. A < A
24 fveq1 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( b ` 0 ) = ( ( <" A "> ++ <" A "> ) ` 0 ) )
25 ccat2s1p1 
 |-  ( A e. _V -> ( ( <" A "> ++ <" A "> ) ` 0 ) = A )
26 1 25 ax-mp 
 |-  ( ( <" A "> ++ <" A "> ) ` 0 ) = A
27 24 26 eqtrdi 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( b ` 0 ) = A )
28 fveq1 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( b ` ( 0 + 1 ) ) = ( ( <" A "> ++ <" A "> ) ` ( 0 + 1 ) ) )
29 1e0p1 
 |-  1 = ( 0 + 1 )
30 29 fveq2i 
 |-  ( ( <" A "> ++ <" A "> ) ` 1 ) = ( ( <" A "> ++ <" A "> ) ` ( 0 + 1 ) )
31 ccat2s1p2 
 |-  ( A e. _V -> ( ( <" A "> ++ <" A "> ) ` 1 ) = A )
32 1 31 ax-mp 
 |-  ( ( <" A "> ++ <" A "> ) ` 1 ) = A
33 30 32 eqtr3i 
 |-  ( ( <" A "> ++ <" A "> ) ` ( 0 + 1 ) ) = A
34 28 33 eqtrdi 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( b ` ( 0 + 1 ) ) = A )
35 27 34 breq12d 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( ( b ` 0 ) < ( b ` ( 0 + 1 ) ) <-> A < A ) )
36 23 35 mtbiri 
 |-  ( b = ( <" A "> ++ <" A "> ) -> -. ( b ` 0 ) < ( b ` ( 0 + 1 ) ) )
37 fveq2 
 |-  ( k = 0 -> ( b ` k ) = ( b ` 0 ) )
38 fvoveq1 
 |-  ( k = 0 -> ( b ` ( k + 1 ) ) = ( b ` ( 0 + 1 ) ) )
39 37 38 breq12d 
 |-  ( k = 0 -> ( ( b ` k ) < ( b ` ( k + 1 ) ) <-> ( b ` 0 ) < ( b ` ( 0 + 1 ) ) ) )
40 39 biimpd 
 |-  ( k = 0 -> ( ( b ` k ) < ( b ` ( k + 1 ) ) -> ( b ` 0 ) < ( b ` ( 0 + 1 ) ) ) )
41 40 con3d 
 |-  ( k = 0 -> ( -. ( b ` 0 ) < ( b ` ( 0 + 1 ) ) -> -. ( b ` k ) < ( b ` ( k + 1 ) ) ) )
42 36 41 syl5com 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( k = 0 -> -. ( b ` k ) < ( b ` ( k + 1 ) ) ) )
43 22 42 jcad 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( k = 0 -> ( k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) /\ -. ( b ` k ) < ( b ` ( k + 1 ) ) ) ) )
44 43 eximdv 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( E. k k = 0 -> E. k ( k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) /\ -. ( b ` k ) < ( b ` ( k + 1 ) ) ) ) )
45 4 44 mpi 
 |-  ( b = ( <" A "> ++ <" A "> ) -> E. k ( k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) /\ -. ( b ` k ) < ( b ` ( k + 1 ) ) ) )
46 nfre1 
 |-  F/ k E. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) -. ( b ` k ) < ( b ` ( k + 1 ) )
47 rspe 
 |-  ( ( k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) /\ -. ( b ` k ) < ( b ` ( k + 1 ) ) ) -> E. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) -. ( b ` k ) < ( b ` ( k + 1 ) ) )
48 46 47 exlimi 
 |-  ( E. k ( k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) /\ -. ( b ` k ) < ( b ` ( k + 1 ) ) ) -> E. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) -. ( b ` k ) < ( b ` ( k + 1 ) ) )
49 45 48 syl 
 |-  ( b = ( <" A "> ++ <" A "> ) -> E. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) -. ( b ` k ) < ( b ` ( k + 1 ) ) )
50 rexnal 
 |-  ( E. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) -. ( b ` k ) < ( b ` ( k + 1 ) ) <-> -. A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) )
51 49 50 sylib 
 |-  ( b = ( <" A "> ++ <" A "> ) -> -. A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) )
52 df-upword 
 |-  UpWord S = { b | ( b e. Word S /\ A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) ) }
53 52 eqabri 
 |-  ( b e. UpWord S <-> ( b e. Word S /\ A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) ) )
54 53 simprbi 
 |-  ( b e. UpWord S -> A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) )
55 51 54 nsyl 
 |-  ( b = ( <" A "> ++ <" A "> ) -> -. b e. UpWord S )
56 eleq1 
 |-  ( b = ( <" A "> ++ <" A "> ) -> ( b e. UpWord S <-> ( <" A "> ++ <" A "> ) e. UpWord S ) )
57 55 56 mtbid 
 |-  ( b = ( <" A "> ++ <" A "> ) -> -. ( <" A "> ++ <" A "> ) e. UpWord S )
58 2 57 vtocle 
 |-  -. ( <" A "> ++ <" A "> ) e. UpWord S