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∈V
Assertion tworepnotupword Could not format assertion : No typesetting found for |- -. ( <" A "> ++ <" A "> ) e. UpWord S with typecode |-

Proof

Step Hyp Ref Expression
1 tworepnotupword.1 ⊢A∈V
2 ovex ⊢⟨“A”⟩++⟨“A”⟩∈V
3 c0ex ⊢0∈V
4 3 isseti ⊢∃kk=0
5 0z ⊢0∈ℤ
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∈ℤ
11 9 10 eqeltri ⊢⟨“A”⟩++⟨“A”⟩−1∈ℤ
12 0lt1 ⊢0<1
13 12 9 breqtrri ⊢0<⟨“A”⟩++⟨“A”⟩−1
14 fzolb ⊢0∈0..^⟨“A”⟩++⟨“A”⟩−1↔0∈ℤ∧⟨“A”⟩++⟨“A”⟩−1∈ℤ∧0<⟨“A”⟩++⟨“A”⟩−1
15 5 11 13 14 mpbir3an ⊢0∈0..^⟨“A”⟩++⟨“A”⟩−1
16 eleq1a ⊢0∈0..^⟨“A”⟩++⟨“A”⟩−1→k=0→k∈0..^⟨“A”⟩++⟨“A”⟩−1
17 15 16 ax-mp ⊢k=0→k∈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∈0..^b−1↔k∈0..^⟨“A”⟩++⟨“A”⟩−1
22 17 21 imbitrrid ⊢b=⟨“A”⟩++⟨“A”⟩→k=0→k∈0..^b−1
23 et-ltneverrefl ⊢¬A<A
24 fveq1 ⊢b=⟨“A”⟩++⟨“A”⟩→b⁡0=⟨“A”⟩++⟨“A”⟩⁡0
25 ccat2s1p1 ⊢A∈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∈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∈0..^b−1∧¬b⁡k<b⁡k+1
44 43 eximdv ⊢b=⟨“A”⟩++⟨“A”⟩→∃kk=0→∃kk∈0..^b−1∧¬b⁡k<b⁡k+1
45 4 44 mpi ⊢b=⟨“A”⟩++⟨“A”⟩→∃kk∈0..^b−1∧¬b⁡k<b⁡k+1
46 nfre1 ⊢Ⅎk∃k∈0..^b−1¬b⁡k<b⁡k+1
47 rspe ⊢k∈0..^b−1∧¬b⁡k<b⁡k+1→∃k∈0..^b−1¬b⁡k<b⁡k+1
48 46 47 exlimi ⊢∃kk∈0..^b−1∧¬b⁡k<b⁡k+1→∃k∈0..^b−1¬b⁡k<b⁡k+1
49 45 48 syl ⊢b=⟨“A”⟩++⟨“A”⟩→∃k∈0..^b−1¬b⁡k<b⁡k+1
50 rexnal ⊢∃k∈0..^b−1¬b⁡k<b⁡k+1↔¬∀k∈0..^b−1b⁡k<b⁡k+1
51 49 50 sylib ⊢b=⟨“A”⟩++⟨“A”⟩→¬∀k∈0..^b−1b⁡k<b⁡k+1
52 df-upword Could not format UpWord S = { b | ( b e. Word S /\ A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) ) } : No typesetting found for |- UpWord S = { b | ( b e. Word S /\ A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) ) } with typecode |-
53 52 eqabri Could not format ( b e. UpWord S <-> ( b e. Word S /\ A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) ) ) : No typesetting found for |- ( b e. UpWord S <-> ( b e. Word S /\ A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) ) ) with typecode |-
54 53 simprbi Could not format ( b e. UpWord S -> A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) ) : No typesetting found for |- ( b e. UpWord S -> A. k e. ( 0 ..^ ( ( # ` b ) - 1 ) ) ( b ` k ) < ( b ` ( k + 1 ) ) ) with typecode |-
55 51 54 nsyl Could not format ( b = ( <" A "> ++ <" A "> ) -> -. b e. UpWord S ) : No typesetting found for |- ( b = ( <" A "> ++ <" A "> ) -> -. b e. UpWord S ) with typecode |-
56 eleq1 Could not format ( b = ( <" A "> ++ <" A "> ) -> ( b e. UpWord S <-> ( <" A "> ++ <" A "> ) e. UpWord S ) ) : No typesetting found for |- ( b = ( <" A "> ++ <" A "> ) -> ( b e. UpWord S <-> ( <" A "> ++ <" A "> ) e. UpWord S ) ) with typecode |-
57 55 56 mtbid Could not format ( b = ( <" A "> ++ <" A "> ) -> -. ( <" A "> ++ <" A "> ) e. UpWord S ) : No typesetting found for |- ( b = ( <" A "> ++ <" A "> ) -> -. ( <" A "> ++ <" A "> ) e. UpWord S ) with typecode |-
58 2 57 vtocle Could not format -. ( <" A "> ++ <" A "> ) e. UpWord S : No typesetting found for |- -. ( <" A "> ++ <" A "> ) e. UpWord S with typecode |-