Theorem efgredlem 19659

Description: The reduced word that forms the base of the sequence in efgsval 19643 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 6899	. . . . . . . . . 10 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
3	1, 2	eqsstri 3976	. . . . . . . . 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 19642	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1)))))
11	10	simp1bi 1145	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
12	4, 11	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
13	12	eldifad 3909	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ Word 𝑊)
14		wrdf 14425	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Word 𝑊 → 𝐴:(0..^(♯‘𝐴))⟶𝑊)
15	13, 14	syl 17	. . . . . . . . . 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 19652	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ∈ ℕ))
21	20	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ ℕ)
22		nnm1nn0 12422	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
24	21	nnred 12140	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ ℝ)
25	24	lem1d 12055	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))
26		eldifsni 4739	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ≠ ∅)
27	4, 11, 26	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ ∅)
28		wrdfin 14439	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑊 → 𝐴 ∈ Fin)
29		hashnncl 14273	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
30	13, 28, 29	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
31	27, 30	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
32		nnm1nn0 12422	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐴) ∈ ℕ → ((♯‘𝐴) − 1) ∈ ℕ0)
33		fznn0 13519	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) − 1) ∈ ℕ0 → ((((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)) ↔ ((((♯‘𝐴) − 1) − 1) ∈ ℕ0 ∧ (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))))
34	31, 32, 33	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)) ↔ ((((♯‘𝐴) − 1) − 1) ∈ ℕ0 ∧ (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))))
35	23, 25, 34	mpbir2and 713	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)))
36		lencl 14440	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Word 𝑊 → (♯‘𝐴) ∈ ℕ0)
37	13, 36	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ0)
38	37	nn0zd 12494	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
39		fzoval 13560	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ ℤ → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
40	38, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
41	35, 40	eleqtrrd 2834	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ (0..^(♯‘𝐴)))
42	15, 41	ffvelcdmd 7018	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊)
43	3, 42	sselid 3927	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2o))
44		lencl 14440	. . . . . . . 8 ⊢ ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2o) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℕ0)
45	43, 44	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℕ0)
46	45	nn0red 12443	. . . . . 6 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ)
47		2rp 12895	. . . . . 6 ⊢ 2 ∈ ℝ+
48		ltaddrp 12929	. . . . . 6 ⊢ (((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ ∧ 2 ∈ ℝ+) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
49	46, 47, 48	sylancl 586	. . . . 5 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
50	37	nn0red 12443	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℝ)
51	50	lem1d 12055	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
52		fznn 13492	. . . . . . . . . . 11 ⊢ ((♯‘𝐴) ∈ ℤ → (((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)) ↔ (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴))))
53	38, 52	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)) ↔ (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴))))
54	21, 51, 53	mpbir2and 713	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)))
55	1, 5, 6, 7, 8, 9	efgsres 19650	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴))) → (𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆)
56	4, 54, 55	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆)
57	1, 5, 6, 7, 8, 9	efgsval 19643	. . . . . . . 8 ⊢ ((𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)))
58	56, 57	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)))
59		fz1ssfz0 13523	. . . . . . . . . . . 12 ⊢ (1...(♯‘𝐴)) ⊆ (0...(♯‘𝐴))
60	59, 54	sselid 3927	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴)))
61		pfxres 14587	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1))))
62	13, 60, 61	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1))))
63	62	fveq2d 6826	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))))
64		pfxlen 14591	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
65	13, 60, 64	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
66	63, 65	eqtr3d 2768	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((♯‘𝐴) − 1))
67	66	fvoveq1d 7368	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)))
68		fzo0end 13658	. . . . . . . 8 ⊢ (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ (0..^((♯‘𝐴) − 1)))
69		fvres 6841	. . . . . . . 8 ⊢ ((((♯‘𝐴) − 1) − 1) ∈ (0..^((♯‘𝐴) − 1)) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
70	21, 68, 69	3syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
71	58, 67, 70	3eqtrd 2770	. . . . . 6 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
72	71	fveq2d 6826	. . . . 5 ⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) = (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
73	1, 5, 6, 7, 8, 9	efgsdmi 19644	. . . . . . 7 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
74	4, 21, 73	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
75	1, 5, 6, 7	efgtlen 19638	. . . . . 6 ⊢ (((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
76	42, 74, 75	syl2anc 584	. . . . 5 ⊢ (𝜑 → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
77	49, 72, 76	3brtr4d 5121	. . . 4 ⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)))
78	1, 5, 6, 7	efgtf 19634	. . . . . . . . . . . 12 ⊢ ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊 → ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐴‘(((♯‘𝐴) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊))
79	42, 78	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐴‘(((♯‘𝐴) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊))
80	79	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊)
81		ffn 6651	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn ((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o)))
82		ovelrn 7522	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn ((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o)) → ((𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ↔ ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟)))
83	80, 81, 82	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ↔ ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟)))
84	74, 83	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟))
85	20	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐵) − 1) ∈ ℕ)
86	1, 5, 6, 7, 8, 9	efgsdmi 19644	. . . . . . . . . 10 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
87	17, 85, 86	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
88	1, 5, 6, 7, 8, 9	efgsdm 19642	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1)))))
89	88	simp1bi 1145	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
90	17, 89	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
91	90	eldifad 3909	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ Word 𝑊)
92		wrdf 14425	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(♯‘𝐵))⟶𝑊)
93	91, 92	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵:(0..^(♯‘𝐵))⟶𝑊)
94		fzo0end 13658	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐵) − 1) ∈ ℕ → (((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)))
95		elfzofz 13575	. . . . . . . . . . . . . . 15 ⊢ ((((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → (((♯‘𝐵) − 1) − 1) ∈ (0...((♯‘𝐵) − 1)))
96	85, 94, 95	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0...((♯‘𝐵) − 1)))
97		lencl 14440	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ Word 𝑊 → (♯‘𝐵) ∈ ℕ0)
98	91, 97	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
99	98	nn0zd 12494	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐵) ∈ ℤ)
100		fzoval 13560	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐵) ∈ ℤ → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
101	99, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
102	96, 101	eleqtrrd 2834	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0..^(♯‘𝐵)))
103	93, 102	ffvelcdmd 7018	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊)
104	1, 5, 6, 7	efgtf 19634	. . . . . . . . . . . 12 ⊢ ((𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊 → ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐵‘(((♯‘𝐵) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊))
105	103, 104	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐵‘(((♯‘𝐵) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊))
106	105	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊)
107		ffn 6651	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn ((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o)))
108		ovelrn 7522	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn ((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o)) → ((𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) ↔ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
109	106, 107, 108	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) ↔ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
110	87, 109	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))
111		reeanv 3204	. . . . . . . . 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 3204	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (𝐼 × 2o)∃𝑠 ∈ (𝐼 × 2o)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
113	16	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
114	4	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝐴 ∈ dom 𝑆)
115	17	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝐵 ∈ dom 𝑆)
116	18	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑆‘𝐵))
117	19	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ¬ (𝐴‘0) = (𝐵‘0))
118		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) − 1) − 1) = (((♯‘𝐴) − 1) − 1)
119		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐵) − 1) − 1) = (((♯‘𝐵) − 1) − 1)
120		simpllr 775	. . . . . . . . . . . . . . . 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 494	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))))
122	120	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))
123		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)))
124	123	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑟 ∈ (𝐼 × 2o))
125	123	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑠 ∈ (𝐼 × 2o))
126		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
127	126	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟))
128	126	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))
129		simpr 484	. . . . . . . . . . . . . . 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 19658	. . . . . . . . . . . . . 14 ⊢ ¬ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
131		iman 401	. . . . . . . . . . . . . 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 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
133	132	expr 456	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ (𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o))) → (((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
134	133	rexlimdvva 3189	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) → (∃𝑟 ∈ (𝐼 × 2o)∃𝑠 ∈ (𝐼 × 2o)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
135	112, 134	biimtrrid 243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) → ((∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
136	135	rexlimdvva 3189	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
137	111, 136	biimtrrid 243	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
138	84, 110, 137	mp2and 699	. . . . . . 7 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
139		fvres 6841	. . . . . . . 8 ⊢ ((((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
140	85, 94, 139	3syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
141	138, 70, 140	3eqtr4d 2776	. . . . . 6 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
142		fz1ssfz0 13523	. . . . . . . . . . 11 ⊢ (1...(♯‘𝐵)) ⊆ (0...(♯‘𝐵))
143	98	nn0red 12443	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐵) ∈ ℝ)
144	143	lem1d 12055	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
145		fznn 13492	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) ∈ ℤ → (((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)) ↔ (((♯‘𝐵) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵))))
146	99, 145	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)) ↔ (((♯‘𝐵) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵))))
147	85, 144, 146	mpbir2and 713	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)))
148	142, 147	sselid 3927	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵)))
149		pfxres 14587	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1))))
150	91, 148, 149	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1))))
151	150	fveq2d 6826	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
152		pfxlen 14591	. . . . . . . . 9 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
153	91, 148, 152	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
154	151, 153	eqtr3d 2768	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((♯‘𝐵) − 1))
155	154	fvoveq1d 7368	. . . . . 6 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
156	141, 67, 155	3eqtr4d 2776	. . . . 5 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
157	1, 5, 6, 7, 8, 9	efgsres 19650	. . . . . . 7 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵))) → (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆)
158	17, 147, 157	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆)
159	1, 5, 6, 7, 8, 9	efgsval 19643	. . . . . 6 ⊢ ((𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
160	158, 159	syl 17	. . . . 5 ⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
161	156, 58, 160	3eqtr4d 2776	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
162		fveq2 6822	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))))
163	162	fveq2d 6826	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (♯‘(𝑆‘𝑎)) = (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))))
164	163	breq1d 5099	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) ↔ (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴))))
165	162	eqeq1d 2733	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏)))
166		fveq1 6821	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0))
167	166	eqeq1d 2733	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)))
168	165, 167	imbi12d 344	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))))
169	164, 168	imbi12d 344	. . . . . 6 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)))))
170		fveq2 6822	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑆‘𝑏) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
171	170	eqeq2d 2742	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))))
172		fveq1 6821	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))
173	172	eqeq2d 2742	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0)))
174	171, 173	imbi12d 344	. . . . . . 7 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))))
175	174	imbi2d 340	. . . . . 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 3584	. . . . 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 837	. . . 4 ⊢ (𝜑 → ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))))
178	77, 161, 177	mp2d 49	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))
179		lbfzo0 13599	. . . . 5 ⊢ (0 ∈ (0..^((♯‘𝐴) − 1)) ↔ ((♯‘𝐴) − 1) ∈ ℕ)
180	21, 179	sylibr 234	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((♯‘𝐴) − 1)))
181	180	fvresd 6842	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝐴‘0))
182		lbfzo0 13599	. . . . 5 ⊢ (0 ∈ (0..^((♯‘𝐵) − 1)) ↔ ((♯‘𝐵) − 1) ∈ ℕ)
183	85, 182	sylibr 234	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((♯‘𝐵) − 1)))
184	183	fvresd 6842	. . 3 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝐵‘0))
185	178, 181, 184	3eqtr3d 2774	. 2 ⊢ (𝜑 → (𝐴‘0) = (𝐵‘0))
186	185, 19	pm2.65i 194	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  {crab 3395   ∖ cdif 3894  ∅c0 4280  {csn 4573  ⟨cop 4579  ⟨cotp 4581  ∪ ciun 4939   class class class wbr 5089   ↦ cmpt 5170   I cid 5508   × cxp 5612  dom cdm 5614  ran crn 5615   ↾ cres 5616   Fn wfn 6476  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346   ∈ cmpo 7348  1_oc1o 8378  2_oc2o 8379  Fincfn 8869  ℝcr 11005  0cc0 11006  1c1 11007   + caddc 11009   < clt 11146   ≤ cle 11147   − cmin 11344  ℕcn 12125  2c2 12180  ℕ₀cn0 12381  ℤcz 12468  ℝ⁺crp 12890  ...cfz 13407  ..^cfzo 13554  ♯chash 14237  Word cword 14420   prefix cpfx 14578   splice csplice 14656  ⟨“cs2 14748   ~_FG cefg 19618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-ot 4582  df-uni 4857  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-2o 8386  df-er 8622  df-map 8752  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873  df-card 9832  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-nn 12126  df-2 12188  df-n0 12382  df-xnn0 12455  df-z 12469  df-uz 12733  df-rp 12891  df-fz 13408  df-fzo 13555  df-hash 14238  df-word 14421  df-concat 14478  df-s1 14504  df-substr 14549  df-pfx 14579  df-splice 14657  df-s2 14755

This theorem is referenced by:  efgred  19660