Theorem efgredlem 19961

Description: The reduced word that forms the base of the sequence in efgsval 19945 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 6962	. . . . . . . . . 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 19944	. . . . . . . . . . . . . 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 14663	. . . . . . . . . . 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 19954	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ∈ ℕ))
21	20	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ ℕ)
22		nnm1nn0 12647	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
23	21, 22	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
24	21	nnred 12350	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ ℝ)
25	24	lem1d 12250	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))
26		eldifsni 4753	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ≠ ∅)
27	4, 11, 26	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ ∅)
28		wrdfin 14677	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑊 → 𝐴 ∈ Fin)
29		hashnncl 14510	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
30	13, 28, 29	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
31	27, 30	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
32		nnm1nn0 12647	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐴) ∈ ℕ → ((♯‘𝐴) − 1) ∈ ℕ0)
33		fznn0 13753	. . . . . . . . . . . . 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 14678	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Word 𝑊 → (♯‘𝐴) ∈ ℕ0)
37	13, 36	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ0)
38	37	nn0zd 12718	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
39		fzoval 13794	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ ℤ → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
40	38, 39	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
41	35, 40	eleqtrrd 2864	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ (0..^(♯‘𝐴)))
42	15, 41	ffvelcdmd 7085	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊)
43	3, 42	sselid 3929	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2o))
44		lencl 14678	. . . . . . . 8 ⊢ ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2o) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℕ0)
45	43, 44	syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℕ0)
46	45	nn0red 12668	. . . . . 6 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ)
47		2rp 13125	. . . . . 6 ⊢ 2 ∈ ℝ+
48		ltaddrp 13159	. . . . . 6 ⊢ (((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ ∧ 2 ∈ ℝ+) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
49	46, 47, 48	sylancl 598	. . . . 5 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
50	37	nn0red 12668	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℝ)
51	50	lem1d 12250	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
52		fznn 13726	. . . . . . . . . . 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 19952	. . . . . . . . 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 19945	. . . . . . . 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 13757	. . . . . . . . . . . 12 ⊢ (1...(♯‘𝐴)) ⊆ (0...(♯‘𝐴))
60	59, 54	sselid 3929	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴)))
61		pfxres 14829	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1))))
62	13, 60, 61	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1))))
63	62	fveq2d 6889	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))))
64		pfxlen 14833	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
65	13, 60, 64	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
66	63, 65	eqtr3d 2798	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((♯‘𝐴) − 1))
67	66	fvoveq1d 7442	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)))
68		fzo0end 13893	. . . . . . . 8 ⊢ (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ (0..^((♯‘𝐴) − 1)))
69		fvres 6904	. . . . . . . 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 2800	. . . . . 6 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
72	71	fveq2d 6889	. . . . 5 ⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) = (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
73	1, 5, 6, 7, 8, 9	efgsdmi 19946	. . . . . . 7 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
74	4, 21, 73	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
75	1, 5, 6, 7	efgtlen 19940	. . . . . 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 19936	. . . . . . . . . . . 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 6709	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn ((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o)))
82		ovelrn 7597	. . . . . . . . . 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 19946	. . . . . . . . . 10 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
87	17, 85, 86	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
88	1, 5, 6, 7, 8, 9	efgsdm 19944	. . . . . . . . . . . . . . . . 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 14663	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(♯‘𝐵))⟶𝑊)
93	91, 92	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵:(0..^(♯‘𝐵))⟶𝑊)
94		fzo0end 13893	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐵) − 1) ∈ ℕ → (((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)))
95		elfzofz 13810	. . . . . . . . . . . . . . 15 ⊢ ((((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → (((♯‘𝐵) − 1) − 1) ∈ (0...((♯‘𝐵) − 1)))
96	85, 94, 95	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0...((♯‘𝐵) − 1)))
97		lencl 14678	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ Word 𝑊 → (♯‘𝐵) ∈ ℕ0)
98	91, 97	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
99	98	nn0zd 12718	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐵) ∈ ℤ)
100		fzoval 13794	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐵) ∈ ℤ → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
101	99, 100	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
102	96, 101	eleqtrrd 2864	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0..^(♯‘𝐵)))
103	93, 102	ffvelcdmd 7085	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊)
104	1, 5, 6, 7	efgtf 19936	. . . . . . . . . . . 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 6709	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn ((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o)))
108		ovelrn 7597	. . . . . . . . . 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 3235	. . . . . . . . 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 3235	. . . . . . . . . . 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 2761	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) − 1) − 1) = (((♯‘𝐴) − 1) − 1)
119		eqid 2761	. . . . . . . . . . . . . . 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 19960	. . . . . . . . . . . . . 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 3220	. . . . . . . . . . 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 3220	. . . . . . . . 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 6904	. . . . . . . 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 2806	. . . . . 6 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
142		fz1ssfz0 13757	. . . . . . . . . . 11 ⊢ (1...(♯‘𝐵)) ⊆ (0...(♯‘𝐵))
143	98	nn0red 12668	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐵) ∈ ℝ)
144	143	lem1d 12250	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
145		fznn 13726	. . . . . . . . . . . . 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 14829	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1))))
150	91, 148, 149	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1))))
151	150	fveq2d 6889	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
152		pfxlen 14833	. . . . . . . . 9 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
153	91, 148, 152	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
154	151, 153	eqtr3d 2798	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((♯‘𝐵) − 1))
155	154	fvoveq1d 7442	. . . . . 6 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
156	141, 67, 155	3eqtr4d 2806	. . . . 5 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
157	1, 5, 6, 7, 8, 9	efgsres 19952	. . . . . . 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 19945	. . . . . 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 2806	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
162		fveq2 6885	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))))
163	162	fveq2d 6889	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (♯‘(𝑆‘𝑎)) = (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))))
164	163	breq1d 5113	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) ↔ (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴))))
165	162	eqeq1d 2763	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏)))
166		fveq1 6884	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0))
167	166	eqeq1d 2763	. . . . . . . 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 6885	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑆‘𝑏) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
171	170	eqeq2d 2772	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))))
172		fveq1 6884	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))
173	172	eqeq2d 2772	. . . . . . . 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 13834	. . . . 5 ⊢ (0 ∈ (0..^((♯‘𝐴) − 1)) ↔ ((♯‘𝐴) − 1) ∈ ℕ)
180	21, 179	sylibr 237	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((♯‘𝐴) − 1)))
181	180	fvresd 6905	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝐴‘0))
182		lbfzo0 13834	. . . . 5 ⊢ (0 ∈ (0..^((♯‘𝐵) − 1)) ↔ ((♯‘𝐵) − 1) ∈ ℕ)
183	85, 182	sylibr 237	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((♯‘𝐵) − 1)))
184	183	fvresd 6905	. . 3 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝐵‘0))
185	178, 181, 184	3eqtr3d 2804	. 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 2956  ∀wral 3077  ∃wrex 3087  {crab 3413   ∖ cdif 3896  ∅c0 4279  {csn 4584  ⟨cop 4590  ⟨cotp 4592  ∪ ciun 4951   class class class wbr 5103   ↦ cmpt 5186   I cid 5545   × cxp 5649  dom cdm 5651  ran crn 5652   ↾ cres 5653   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422  1_oc1o 8469  2_oc2o 8470  Fincfn 8973  ℝcr 11199  0cc0 11200  1c1 11201   + caddc 11203   < clt 11343   ≤ cle 11344   − cmin 11541  ℕcn 12335  2c2 12397  ℕ₀cn0 12606  ℤcz 12693  ℝ⁺crp 13120  ...cfz 13639  ..^cfzo 13788  ♯chash 14474  Word cword 14658   prefix cpfx 14820   splice csplice 14898  ⟨“cs2 14992   ~_FG cefg 19920

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 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  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 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-2o 8477  df-er 8717  df-map 8849  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-card 10020  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-2 12405  df-n0 12607  df-xnn0 12680  df-z 12694  df-uz 12966  df-rp 13121  df-fz 13640  df-fzo 13789  df-hash 14475  df-word 14659  df-concat 14716  df-s1 14743  df-substr 14789  df-pfx 14821  df-splice 14899  df-s2 14999

This theorem is used by:  efgred  19962