Theorem efgredlem 19626

Description: The reduced word that forms the base of the sequence in efgsval 19610 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 6900	. . . . . . . . . 10 ⊢ ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
3	1, 2	eqsstri 3982	. . . . . . . . 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 19609	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1)))))
11	10	simp1bi 1145	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
12	4, 11	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
13	12	eldifad 3915	. . . . . . . . . . 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 19619	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ∈ ℕ))
21	20	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ ℕ)
22		nnm1nn0 12425	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
24	21	nnred 12143	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ ℝ)
25	24	lem1d 12058	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))
26		eldifsni 4741	. . . . . . . . . . . . . . 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 12425	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐴) ∈ ℕ → ((♯‘𝐴) − 1) ∈ ℕ0)
33		fznn0 13522	. . . . . . . . . . . . 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 12497	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
39		fzoval 13563	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ ℤ → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
40	38, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
41	35, 40	eleqtrrd 2831	. . . . . . . . . 10 ⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ (0..^(♯‘𝐴)))
42	15, 41	ffvelcdmd 7019	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊)
43	3, 42	sselid 3933	. . . . . . . 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 12446	. . . . . 6 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ)
47		2rp 12898	. . . . . 6 ⊢ 2 ∈ ℝ+
48		ltaddrp 12932	. . . . . 6 ⊢ (((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ ∧ 2 ∈ ℝ+) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
49	46, 47, 48	sylancl 586	. . . . 5 ⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
50	37	nn0red 12446	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐴) ∈ ℝ)
51	50	lem1d 12058	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
52		fznn 13495	. . . . . . . . . . 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 19617	. . . . . . . . 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 19610	. . . . . . . 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 13526	. . . . . . . . . . . 12 ⊢ (1...(♯‘𝐴)) ⊆ (0...(♯‘𝐴))
60	59, 54	sselid 3933	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴)))
61		pfxres 14586	. . . . . . . . . . 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 14590	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
65	13, 60, 64	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
66	63, 65	eqtr3d 2766	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((♯‘𝐴) − 1))
67	66	fvoveq1d 7371	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)))
68		fzo0end 13661	. . . . . . . 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 2768	. . . . . 6 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
72	71	fveq2d 6826	. . . . 5 ⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) = (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
73	1, 5, 6, 7, 8, 9	efgsdmi 19611	. . . . . . 7 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
74	4, 21, 73	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
75	1, 5, 6, 7	efgtlen 19605	. . . . . 6 ⊢ (((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
76	42, 74, 75	syl2anc 584	. . . . 5 ⊢ (𝜑 → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
77	49, 72, 76	3brtr4d 5124	. . . 4 ⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴)))
78	1, 5, 6, 7	efgtf 19601	. . . . . . . . . . . 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 6652	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn ((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o)))
82		ovelrn 7525	. . . . . . . . . 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 19611	. . . . . . . . . 10 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
87	17, 85, 86	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
88	1, 5, 6, 7, 8, 9	efgsdm 19609	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1)))))
89	88	simp1bi 1145	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
90	17, 89	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
91	90	eldifad 3915	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ Word 𝑊)
92		wrdf 14425	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(♯‘𝐵))⟶𝑊)
93	91, 92	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵:(0..^(♯‘𝐵))⟶𝑊)
94		fzo0end 13661	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐵) − 1) ∈ ℕ → (((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)))
95		elfzofz 13578	. . . . . . . . . . . . . . 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 12497	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐵) ∈ ℤ)
100		fzoval 13563	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐵) ∈ ℤ → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
101	99, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
102	96, 101	eleqtrrd 2831	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0..^(♯‘𝐵)))
103	93, 102	ffvelcdmd 7019	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊)
104	1, 5, 6, 7	efgtf 19601	. . . . . . . . . . . 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 6652	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn ((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o)))
108		ovelrn 7525	. . . . . . . . . 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 3201	. . . . . . . . 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 3201	. . . . . . . . . . 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 2729	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) − 1) − 1) = (((♯‘𝐴) − 1) − 1)
119		eqid 2729	. . . . . . . . . . . . . . 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 19625	. . . . . . . . . . . . . 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 3186	. . . . . . . . . . 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 3186	. . . . . . . . 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 2774	. . . . . 6 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
142		fz1ssfz0 13526	. . . . . . . . . . 11 ⊢ (1...(♯‘𝐵)) ⊆ (0...(♯‘𝐵))
143	98	nn0red 12446	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐵) ∈ ℝ)
144	143	lem1d 12058	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
145		fznn 13495	. . . . . . . . . . . . 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 3933	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵)))
149		pfxres 14586	. . . . . . . . . 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 14590	. . . . . . . . 9 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
153	91, 148, 152	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
154	151, 153	eqtr3d 2766	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((♯‘𝐵) − 1))
155	154	fvoveq1d 7371	. . . . . 6 ⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
156	141, 67, 155	3eqtr4d 2774	. . . . 5 ⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
157	1, 5, 6, 7, 8, 9	efgsres 19617	. . . . . . 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 19610	. . . . . 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 2774	. . . 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 5102	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) ↔ (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆‘𝐴))))
165	162	eqeq1d 2731	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏)))
166		fveq1 6821	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0))
167	166	eqeq1d 2731	. . . . . . . 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 2740	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))))
172		fveq1 6821	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))
173	172	eqeq2d 2740	. . . . . . . 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 3589	. . . . 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 13602	. . . . 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 13602	. . . . 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 2772	. 2 ⊢ (𝜑 → (𝐴‘0) = (𝐵‘0))
186	185, 19	pm2.65i 194	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3394   ∖ cdif 3900  ∅c0 4284  {csn 4577  ⟨cop 4583  ⟨cotp 4585  ∪ ciun 4941   class class class wbr 5092   ↦ cmpt 5173   I cid 5513   × cxp 5617  dom cdm 5619  ran crn 5620   ↾ cres 5621   Fn wfn 6477  ⟶wf 6478  ‘cfv 6482  (class class class)co 7349   ∈ cmpo 7351  1_oc1o 8381  2_oc2o 8382  Fincfn 8872  ℝcr 11008  0cc0 11009  1c1 11010   + caddc 11012   < clt 11149   ≤ cle 11150   − cmin 11347  ℕcn 12128  2c2 12183  ℕ₀cn0 12384  ℤcz 12471  ℝ⁺crp 12893  ...cfz 13410  ..^cfzo 13557  ♯chash 14237  Word cword 14420   prefix cpfx 14577   splice csplice 14655  ⟨“cs2 14748   ~_FG cefg 19585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-ot 4586  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-2o 8389  df-er 8625  df-map 8755  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-card 9835  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-2 12191  df-n0 12385  df-xnn0 12458  df-z 12472  df-uz 12736  df-rp 12894  df-fz 13411  df-fzo 13558  df-hash 14238  df-word 14421  df-concat 14478  df-s1 14503  df-substr 14548  df-pfx 14578  df-splice 14656  df-s2 14755

This theorem is referenced by:  efgred  19627