Theorem tworepnotupword

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

	Ref	Expression
Hypothesis	tworepnotupword.1	⊢ 𝐴 ∈ V
Assertion	tworepnotupword	⊢ ¬ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ∈ UpWord 𝑆

Proof

Step	Hyp	Ref	Expression
1		tworepnotupword.1	⊢ 𝐴 ∈ V
2		ovex	⊢ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ∈ V
3		c0ex	⊢ 0 ∈ V
4	3	isseti	⊢ ∃ 𝑘 𝑘 = 0
5		0z	⊢ 0 ∈ ℤ
6		ccat2s1len	⊢ ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) = 2
7	6	oveq1i	⊢ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) = ( 2 − 1 )
8		2m1e1	⊢ ( 2 − 1 ) = 1
9	7 8	eqtri	⊢ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) = 1
10		1z	⊢ 1 ∈ ℤ
11	9 10	eqeltri	⊢ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ∈ ℤ
12		0lt1	⊢ 0 < 1
13	12 9	breqtrri	⊢ 0 < ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 )
14		fzolb	⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ) ↔ ( 0 ∈ ℤ ∧ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ∈ ℤ ∧ 0 < ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ) )
15	5 11 13 14	mpbir3an	⊢ 0 ∈ ( 0 ..^ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) )
16		eleq1a	⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ) → ( 𝑘 = 0 → 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ) ) )
17	15 16	ax-mp	⊢ ( 𝑘 = 0 → 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ) )
18		fveq2	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) )
19	18	oveq1d	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( ( ♯ ‘ 𝑏 ) − 1 ) = ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) )
20	19	oveq2d	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ) )
21	20	eleq2d	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ↔ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ) − 1 ) ) ) )
22	17 21	imbitrrid	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑘 = 0 → 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ) )
23		et-ltneverrefl	⊢ ¬ 𝐴 < 𝐴
24		fveq1	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑏 ‘ 0 ) = ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ 0 ) )
25		ccat2s1p1	⊢ ( 𝐴 ∈ V → ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ 0 ) = 𝐴 )
26	1 25	ax-mp	⊢ ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ 0 ) = 𝐴
27	24 26	eqtrdi	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑏 ‘ 0 ) = 𝐴 )
28		fveq1	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑏 ‘ ( 0 + 1 ) ) = ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 0 + 1 ) ) )
29		1e0p1	⊢ 1 = ( 0 + 1 )
30	29	fveq2i	⊢ ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ 1 ) = ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 0 + 1 ) )
31		ccat2s1p2	⊢ ( 𝐴 ∈ V → ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ 1 ) = 𝐴 )
32	1 31	ax-mp	⊢ ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ 1 ) = 𝐴
33	30 32	eqtr3i	⊢ ( ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 0 + 1 ) ) = 𝐴
34	28 33	eqtrdi	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑏 ‘ ( 0 + 1 ) ) = 𝐴 )
35	27 34	breq12d	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( ( 𝑏 ‘ 0 ) < ( 𝑏 ‘ ( 0 + 1 ) ) ↔ 𝐴 < 𝐴 ) )
36	23 35	mtbiri	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ¬ ( 𝑏 ‘ 0 ) < ( 𝑏 ‘ ( 0 + 1 ) ) )
37		fveq2	⊢ ( 𝑘 = 0 → ( 𝑏 ‘ 𝑘 ) = ( 𝑏 ‘ 0 ) )
38		fvoveq1	⊢ ( 𝑘 = 0 → ( 𝑏 ‘ ( 𝑘 + 1 ) ) = ( 𝑏 ‘ ( 0 + 1 ) ) )
39	37 38	breq12d	⊢ ( 𝑘 = 0 → ( ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑏 ‘ 0 ) < ( 𝑏 ‘ ( 0 + 1 ) ) ) )
40	39	biimpd	⊢ ( 𝑘 = 0 → ( ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) → ( 𝑏 ‘ 0 ) < ( 𝑏 ‘ ( 0 + 1 ) ) ) )
41	40	con3d	⊢ ( 𝑘 = 0 → ( ¬ ( 𝑏 ‘ 0 ) < ( 𝑏 ‘ ( 0 + 1 ) ) → ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) )
42	36 41	syl5com	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑘 = 0 → ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) )
43	22 42	jcad	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑘 = 0 → ( 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ∧ ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) ) )
44	43	eximdv	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( ∃ 𝑘 𝑘 = 0 → ∃ 𝑘 ( 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ∧ ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) ) )
45	4 44	mpi	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ∃ 𝑘 ( 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ∧ ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) )
46		nfre1	⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) )
47		rspe	⊢ ( ( 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ∧ ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) → ∃ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) )
48	46 47	exlimi	⊢ ( ∃ 𝑘 ( 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ∧ ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) → ∃ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) )
49	45 48	syl	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ∃ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) )
50		rexnal	⊢ ( ∃ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ¬ ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ↔ ¬ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) )
51	49 50	sylib	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ¬ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) )
52		df-upword	⊢ UpWord 𝑆 = { 𝑏 ∣ ( 𝑏 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) }
53	52	eqabri	⊢ ( 𝑏 ∈ UpWord 𝑆 ↔ ( 𝑏 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) ) )
54	53	simprbi	⊢ ( 𝑏 ∈ UpWord 𝑆 → ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑏 ) − 1 ) ) ( 𝑏 ‘ 𝑘 ) < ( 𝑏 ‘ ( 𝑘 + 1 ) ) )
55	51 54	nsyl	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ¬ 𝑏 ∈ UpWord 𝑆 )
56		eleq1	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ( 𝑏 ∈ UpWord 𝑆 ↔ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ∈ UpWord 𝑆 ) )
57	55 56	mtbid	⊢ ( 𝑏 = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) → ¬ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ∈ UpWord 𝑆 )
58	2 57	vtocle	⊢ ¬ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐴 ”⟩ ) ∈ UpWord 𝑆