Theorem efgredlem 19875

Description: The reduced word that forms the base of the sequence in efgsval 19859 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.) (Proof shortened by AV, 3-Nov-2022.)

Hypotheses

Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))
efgval.r	⊢ ∼ = ( ~FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
efgred.d	⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
efgred.s	⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
efgredlem.1	⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
efgredlem.2	⊢ (𝜑 → 𝐴 ∈ dom 𝑆)
efgredlem.3	⊢ (𝜑 → 𝐵 ∈ dom 𝑆)
efgredlem.4	⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))
efgredlem.5	⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))

Assertion

Ref	Expression
efgredlem	⊢ ¬ 𝜑

Distinct variable groups:   𝑎,𝑏,𝐴   𝑦,𝑎,𝑧,𝑏   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧   𝑚,𝑎,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑏   𝑘,𝑎,𝑇,𝑏,𝑚,𝑡,𝑥   𝑊,𝑎,𝑏   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ∼ ,𝑎,𝑏,𝑚,𝑡,𝑥,𝑦,𝑧   𝐵,𝑎,𝑏   𝑆,𝑎,𝑏   𝐼,𝑎,𝑏,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑎,𝑏,𝑚,𝑡

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑡, 𝑘, 𝑚, 𝑛, 𝑎, 𝑏)   𝐴(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑡, 𝑘, 𝑚, 𝑛)   𝐵(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑡, 𝑘, 𝑚, 𝑛)   𝐷(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑘, 𝑛)   ∼ (𝑤, 𝑣, 𝑘, 𝑛)   𝑆(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑡, 𝑘, 𝑚, 𝑛)   𝑇(𝑦, 𝑧, 𝑤, 𝑣, 𝑛)   𝐼(𝑘)   𝑀(𝑦, 𝑧, 𝑘)

Proof of Theorem efgredlem

Dummy variables 𝑖 𝑗 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		efgval.w	. . . . . . . . . 10 ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))
2		fviss 6956	. . . . . . . . . 10 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
3	1, 2	eqsstri 3977	. . . . . . . . 9 ⊢ 𝑊 ⊆ Word (𝐼 × 2o)
4		efgredlem.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)
5		efgval.r	. . . . . . . . . . . . . . 15 ⊢ ∼ = ( ~FG ‘𝐼)
6		efgval2.m	. . . . . . . . . . . . . . 15 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)
7		efgval2.t	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
8		efgred.d	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
9		efgred.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
10	1, 5, 6, 7, 8, 9	efgsdm 19858	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1)))))
11	10	simp1bi 1163	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
12	4, 11	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
13	12	eldifad 3911	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ Word 𝑊)
14		wrdf 14584	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Word 𝑊 → 𝐴:(0..^(♯‘𝐴))⟶𝑊)
15	13, 14	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:(0..^(♯‘𝐴))⟶𝑊)
16		efgredlem.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
17		efgredlem.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)
18		efgredlem.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))
19		efgredlem.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))
20	1, 5, 6, 7, 8, 9, 16, 4, 17, 18, 19	efgredlema 19868	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ∈ ℕ))
21	20	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ ℕ)
22		nnm1nn0 12570	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
23	21, 22	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
24	21	nnred 12273	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ ℝ)
25	24	lem1d 12173	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))
26		eldifsni 4753	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ≠ ∅)
27	4, 11, 26	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ ∅)
28		wrdfin 14598	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑊 → 𝐴 ∈ Fin)
29		hashnncl 14431	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
30	13, 28, 29	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
31	27, 30	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
32		nnm1nn0 12570	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐴) ∈ ℕ → ((♯‘𝐴) − 1) ∈ ℕ0)
33		fznn0 13675	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) − 1) ∈ ℕ0 → ((((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)) ↔ ((((♯‘𝐴) − 1) − 1) ∈ ℕ0 ∧ (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))))
34	31, 32, 33	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)) ↔ ((((♯‘𝐴) − 1) − 1) ∈ ℕ0 ∧ (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))))
35	23, 25, 34	mpbir2and 726	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)))
36		lencl 14599	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Word 𝑊 → (♯‘𝐴) ∈ ℕ0)
37	13, 36	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ0)
38	37	nn0zd 12641	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
39		fzoval 13716	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ ℤ → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
40	38, 39	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
41	35, 40	eleqtrrd 2863	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ (0..^(♯‘𝐴)))
42	15, 41	ffvelcdmd 7079	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊)
43	3, 42	sselid 3929	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2o))
44		lencl 14599	. . . . . . . 8 ⊢ ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2o) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℕ0)
45	43, 44	syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℕ0)
46	45	nn0red 12591	. . . . . 6 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ)
47		2rp 13048	. . . . . 6 ⊢ 2 ∈ ℝ+
48		ltaddrp 13082	. . . . . 6 ⊢ (((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ ∧ 2 ∈ ℝ+) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
49	46, 47, 48	sylancl 598	. . . . 5 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
50	37	nn0red 12591	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℝ)
51	50	lem1d 12173	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
52		fznn 13648	. . . . . . . . . . 11 ⊢ ((♯‘𝐴) ∈ ℤ → (((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)) ↔ (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴))))
53	38, 52	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)) ↔ (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴))))
54	21, 51, 53	mpbir2and 726	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)))
55	1, 5, 6, 7, 8, 9	efgsres 19866	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴))) → (𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆)
56	4, 54, 55	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆)
57	1, 5, 6, 7, 8, 9	efgsval 19859	. . . . . . . 8 ⊢ ((𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)))
58	56, 57	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)))
59		fz1ssfz0 13679	. . . . . . . . . . . 12 ⊢ (1...(♯‘𝐴)) ⊆ (0...(♯‘𝐴))
60	59, 54	sselid 3929	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴)))
61		pfxres 14750	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1))))
62	13, 60, 61	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1))))
63	62	fveq2d 6883	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))))
64		pfxlen 14754	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
65	13, 60, 64	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
66	63, 65	eqtr3d 2797	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((♯‘𝐴) − 1))
67	66	fvoveq1d 7436	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)))
68		fzo0end 13815	. . . . . . . 8 ⊢ (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ (0..^((♯‘𝐴) − 1)))
69		fvres 6898	. . . . . . . 8 ⊢ ((((♯‘𝐴) − 1) − 1) ∈ (0..^((♯‘𝐴) − 1)) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
70	21, 68, 69	3syl 19	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
71	58, 67, 70	3eqtrd 2799	. . . . . 6 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
72	71	fveq2d 6883	. . . . 5 ⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) = (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
73	1, 5, 6, 7, 8, 9	efgsdmi 19860	. . . . . . 7 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
74	4, 21, 73	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
75	1, 5, 6, 7	efgtlen 19854	. . . . . 6 ⊢ (((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
76	42, 74, 75	syl2anc 596	. . . . 5 ⊢ (𝜑 → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
77	49, 72, 76	3brtr4d 5137	. . . 4 ⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)))
78	1, 5, 6, 7	efgtf 19850	. . . . . . . . . . . 12 ⊢ ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊 → ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐴‘(((♯‘𝐴) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊))
79	42, 78	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐴‘(((♯‘𝐴) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊))
80	79	simprd 501	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊)
81		ffn 6703	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn ((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o)))
82		ovelrn 7591	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn ((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o)) → ((𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ↔ ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟)))
83	80, 81, 82	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ↔ ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟)))
84	74, 83	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟))
85	20	simprd 501	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐵) − 1) ∈ ℕ)
86	1, 5, 6, 7, 8, 9	efgsdmi 19860	. . . . . . . . . 10 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
87	17, 85, 86	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
88	1, 5, 6, 7, 8, 9	efgsdm 19858	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1)))))
89	88	simp1bi 1163	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
90	17, 89	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
91	90	eldifad 3911	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ Word 𝑊)
92		wrdf 14584	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(♯‘𝐵))⟶𝑊)
93	91, 92	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵:(0..^(♯‘𝐵))⟶𝑊)
94		fzo0end 13815	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐵) − 1) ∈ ℕ → (((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)))
95		elfzofz 13732	. . . . . . . . . . . . . . 15 ⊢ ((((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → (((♯‘𝐵) − 1) − 1) ∈ (0...((♯‘𝐵) − 1)))
96	85, 94, 95	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0...((♯‘𝐵) − 1)))
97		lencl 14599	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ Word 𝑊 → (♯‘𝐵) ∈ ℕ0)
98	91, 97	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
99	98	nn0zd 12641	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐵) ∈ ℤ)
100		fzoval 13716	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐵) ∈ ℤ → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
101	99, 100	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
102	96, 101	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0..^(♯‘𝐵)))
103	93, 102	ffvelcdmd 7079	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊)
104	1, 5, 6, 7	efgtf 19850	. . . . . . . . . . . 12 ⊢ ((𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊 → ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐵‘(((♯‘𝐵) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊))
105	103, 104	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐵‘(((♯‘𝐵) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊))
106	105	simprd 501	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊)
107		ffn 6703	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn ((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o)))
108		ovelrn 7591	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn ((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o)) → ((𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) ↔ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
109	106, 107, 108	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) ↔ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
110	87, 109	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))
111		reeanv 3234	. . . . . . . . 9 ⊢ (∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
112		reeanv 3234	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (𝐼 × 2o)∃𝑠 ∈ (𝐼 × 2o)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
113	16	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
114	4	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝐴 ∈ dom 𝑆)
115	17	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝐵 ∈ dom 𝑆)
116	18	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑆‘𝐵))
117	19	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ¬ (𝐴‘0) = (𝐵‘0))
118		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) − 1) − 1) = (((♯‘𝐴) − 1) − 1)
119		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐵) − 1) − 1) = (((♯‘𝐵) − 1) − 1)
120		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))))
121	120	simpld 500	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))))
122	120	simprd 501	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))
123		simplrl 789	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)))
124	123	simpld 500	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑟 ∈ (𝐼 × 2o))
125	123	simprd 501	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑠 ∈ (𝐼 × 2o))
126		simplrr 790	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
127	126	simpld 500	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟))
128	126	simprd 501	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))
129		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
130	1, 5, 6, 7, 8, 9, 113, 114, 115, 116, 117, 118, 119, 121, 122, 124, 125, 127, 128, 129	efgredlemb 19874	. . . . . . . . . . . . . 14 ⊢ ¬ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
131		iman 407	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) ↔ ¬ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
132	130, 131	mpbir 234	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
133	132	expr 462	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ (𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o))) → (((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
134	133	rexlimdvva 3219	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) → (∃𝑟 ∈ (𝐼 × 2o)∃𝑠 ∈ (𝐼 × 2o)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
135	112, 134	biimtrrid 246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) → ((∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
136	135	rexlimdvva 3219	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
137	111, 136	biimtrrid 246	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
138	84, 110, 137	mp2and 712	. . . . . . 7 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
139		fvres 6898	. . . . . . . 8 ⊢ ((((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
140	85, 94, 139	3syl 19	. . . . . . 7 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
141	138, 70, 140	3eqtr4d 2805	. . . . . 6 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
142		fz1ssfz0 13679	. . . . . . . . . . 11 ⊢ (1...(♯‘𝐵)) ⊆ (0...(♯‘𝐵))
143	98	nn0red 12591	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐵) ∈ ℝ)
144	143	lem1d 12173	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
145		fznn 13648	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) ∈ ℤ → (((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)) ↔ (((♯‘𝐵) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵))))
146	99, 145	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)) ↔ (((♯‘𝐵) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵))))
147	85, 144, 146	mpbir2and 726	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)))
148	142, 147	sselid 3929	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵)))
149		pfxres 14750	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1))))
150	91, 148, 149	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1))))
151	150	fveq2d 6883	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
152		pfxlen 14754	. . . . . . . . 9 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
153	91, 148, 152	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
154	151, 153	eqtr3d 2797	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((♯‘𝐵) − 1))
155	154	fvoveq1d 7436	. . . . . 6 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
156	141, 67, 155	3eqtr4d 2805	. . . . 5 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
157	1, 5, 6, 7, 8, 9	efgsres 19866	. . . . . . 7 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵))) → (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆)
158	17, 147, 157	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆)
159	1, 5, 6, 7, 8, 9	efgsval 19859	. . . . . 6 ⊢ ((𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
160	158, 159	syl 18	. . . . 5 ⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
161	156, 58, 160	3eqtr4d 2805	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
162		fveq2 6879	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))))
163	162	fveq2d 6883	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (♯‘(𝑆‘𝑎)) = (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))))
164	163	breq1d 5113	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) ↔ (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴))))
165	162	eqeq1d 2762	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏)))
166		fveq1 6878	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0))
167	166	eqeq1d 2762	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)))
168	165, 167	imbi12d 347	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))))
169	164, 168	imbi12d 347	. . . . . 6 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)))))
170		fveq2 6879	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑆‘𝑏) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
171	170	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))))
172		fveq1 6878	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))
173	172	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0)))
174	171, 173	imbi12d 347	. . . . . . 7 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))))
175	174	imbi2d 343	. . . . . 6 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0)))))
176	169, 175	rspc2va 3588	. . . . 5 ⊢ ((((𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆 ∧ (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) → ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))))
177	56, 158, 16, 176	syl21anc 851	. . . 4 ⊢ (𝜑 → ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))))
178	77, 161, 177	mp2d 50	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))
179		lbfzo0 13756	. . . . 5 ⊢ (0 ∈ (0..^((♯‘𝐴) − 1)) ↔ ((♯‘𝐴) − 1) ∈ ℕ)
180	21, 179	sylibr 237	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((♯‘𝐴) − 1)))
181	180	fvresd 6899	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝐴‘0))
182		lbfzo0 13756	. . . . 5 ⊢ (0 ∈ (0..^((♯‘𝐵) − 1)) ↔ ((♯‘𝐵) − 1) ∈ ℕ)
183	85, 182	sylibr 237	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((♯‘𝐵) − 1)))
184	183	fvresd 6899	. . 3 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝐵‘0))
185	178, 181, 184	3eqtr3d 2803	. 2 ⊢ (𝜑 → (𝐴‘0) = (𝐵‘0))
186	185, 19	pm2.65i 196	1 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412   ∖ cdif 3896  ∅c0 4279  {csn 4584  ⟨cop 4590  ⟨cotp 4592  ∪ ciun 4951   class class class wbr 5103   ↦ cmpt 5186   I cid 5549   × cxp 5653  dom cdm 5655  ran crn 5656   ↾ cres 5657   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7414   ∈ cmpo 7416  1_oc1o 8449  2_oc2o 8450  Fincfn 8953  ℝcr 11124  0cc0 11125  1c1 11126   + caddc 11128   < clt 11268   ≤ cle 11269   − cmin 11466  ℕcn 12258  2c2 12320  ℕ₀cn0 12529  ℤcz 12616  ℝ⁺crp 13043  ...cfz 13562  ..^cfzo 13710  ♯chash 14395  Word cword 14579   prefix cpfx 14741   splice csplice 14819  ⟨“cs2 14913   ~_FG cefg 19834

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11181  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-ot 4593  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8456  df-2o 8457  df-er 8697  df-map 8829  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-card 9945  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-nn 12259  df-2 12328  df-n0 12530  df-xnn0 12603  df-z 12617  df-uz 12889  df-rp 13044  df-fz 13563  df-fzo 13711  df-hash 14396  df-word 14580  df-concat 14637  df-s1 14664  df-substr 14710  df-pfx 14742  df-splice 14820  df-s2 14920

This theorem is used by:  efgred  19876