efgredlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > efgredlem		Structured version Visualization version GIF version

Theorem efgredlem 18160

Description: The reduced word that forms the base of the sequence in efgsval 18144 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.)

**Hypotheses**
Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2_𝑜))
efgval.r	⊢ ∼ = ( ~_FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_𝑜 ↦ ⟨𝑦, (1_𝑜 ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2_𝑜) ↦ (𝑣 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 (𝐼 × 2_𝑜))
2		fviss 6256	. . . . . . . . . 10 ⊢ ( I ‘Word (𝐼 × 2_𝑜)) ⊆ Word (𝐼 × 2_𝑜)
3	1, 2	eqsstri 3635	. . . . . . . . 9 ⊢ 𝑊 ⊆ Word (𝐼 × 2_𝑜)
4		efgredlem.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)
5		efgval.r	. . . . . . . . . . . . . . 15 ⊢ ∼ = ( ~_FG ‘𝐼)
6		efgval2.m	. . . . . . . . . . . . . . 15 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_𝑜 ↦ ⟨𝑦, (1_𝑜 ∖ 𝑧)⟩)
7		efgval2.t	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2_𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
8		efgred.d	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
9		efgred.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
10	1, 5, 6, 7, 8, 9	efgsdm 18143	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1)))))
11	10	simp1bi 1076	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
12	4, 11	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
13	12	eldifad 3586	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ Word 𝑊)
14		wrdf 13310	. . . . . . . . . . 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 18153	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ∈ ℕ))
21	20	simpld 475	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ ℕ)
22		nnm1nn0 11334	. . . . . . . . . . . . 13 ⊢ (((#‘𝐴) − 1) ∈ ℕ → (((#‘𝐴) − 1) − 1) ∈ ℕ₀)
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ ℕ₀)
24	21	nnred 11035	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ ℝ)
25	24	lem1d 10957	. . . . . . . . . . . 12 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ≤ ((#‘𝐴) − 1))
26		eldifsni 4320	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ≠ ∅)
27	4, 11, 26	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ ∅)
28		wrdfin 13323	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑊 → 𝐴 ∈ Fin)
29		hashnncl 13157	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
30	13, 28, 29	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
31	27, 30	mpbird 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ)
32		nnm1nn0 11334	. . . . . . . . . . . . 13 ⊢ ((#‘𝐴) ∈ ℕ → ((#‘𝐴) − 1) ∈ ℕ₀)
33		fznn0 12432	. . . . . . . . . . . . 13 ⊢ (((#‘𝐴) − 1) ∈ ℕ₀ → ((((#‘𝐴) − 1) − 1) ∈ (0...((#‘𝐴) − 1)) ↔ ((((#‘𝐴) − 1) − 1) ∈ ℕ₀ ∧ (((#‘𝐴) − 1) − 1) ≤ ((#‘𝐴) − 1))))
34	31, 32, 33	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((#‘𝐴) − 1) − 1) ∈ (0...((#‘𝐴) − 1)) ↔ ((((#‘𝐴) − 1) − 1) ∈ ℕ₀ ∧ (((#‘𝐴) − 1) − 1) ≤ ((#‘𝐴) − 1))))
35	23, 25, 34	mpbir2and 957	. . . . . . . . . . 11 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ (0...((#‘𝐴) − 1)))
36		lencl 13324	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Word 𝑊 → (#‘𝐴) ∈ ℕ₀)
37	13, 36	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ₀)
38	37	nn0zd 11480	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐴) ∈ ℤ)
39		fzoval 12471	. . . . . . . . . . . 12 ⊢ ((#‘𝐴) ∈ ℤ → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1)))
40	38, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1)))
41	35, 40	eleqtrrd 2704	. . . . . . . . . 10 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ (0..^(#‘𝐴)))
42	15, 41	ffvelrnd 6360	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) ∈ 𝑊)
43	3, 42	sseldi 3601	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2_𝑜))
44		lencl 13324	. . . . . . . 8 ⊢ ((𝐴‘(((#‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2_𝑜) → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℕ₀)
45	43, 44	syl 17	. . . . . . 7 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℕ₀)
46	45	nn0red 11352	. . . . . 6 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℝ)
47		2rp 11837	. . . . . 6 ⊢ 2 ∈ ℝ⁺
48		ltaddrp 11867	. . . . . 6 ⊢ (((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℝ ∧ 2 ∈ ℝ⁺) → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) < ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
49	46, 47, 48	sylancl 694	. . . . 5 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) < ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
50	37	nn0red 11352	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝐴) ∈ ℝ)
51	50	lem1d 10957	. . . . . . . . . 10 ⊢ (𝜑 → ((#‘𝐴) − 1) ≤ (#‘𝐴))
52		fznn 12408	. . . . . . . . . . 11 ⊢ ((#‘𝐴) ∈ ℤ → (((#‘𝐴) − 1) ∈ (1...(#‘𝐴)) ↔ (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐴) − 1) ≤ (#‘𝐴))))
53	38, 52	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (((#‘𝐴) − 1) ∈ (1...(#‘𝐴)) ↔ (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐴) − 1) ≤ (#‘𝐴))))
54	21, 51, 53	mpbir2and 957	. . . . . . . . 9 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ (1...(#‘𝐴)))
55	1, 5, 6, 7, 8, 9	efgsres 18151	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((#‘𝐴) − 1) ∈ (1...(#‘𝐴))) → (𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆)
56	4, 54, 55	syl2anc 693	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆)
57	1, 5, 6, 7, 8, 9	efgsval 18144	. . . . . . . 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		1eluzge0 11732	. . . . . . . . . . . . . 14 ⊢ 1 ∈ (ℤ_≥‘0)
60		fzss1 12380	. . . . . . . . . . . . . 14 ⊢ (1 ∈ (ℤ_≥‘0) → (1...(#‘𝐴)) ⊆ (0...(#‘𝐴)))
61	59, 60	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1...(#‘𝐴)) ⊆ (0...(#‘𝐴))
62	61, 54	sseldi 3601	. . . . . . . . . . . 12 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ (0...(#‘𝐴)))
63		swrd0val 13421	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((#‘𝐴) − 1) ∈ (0...(#‘𝐴))) → (𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩) = (𝐴 ↾ (0..^((#‘𝐴) − 1))))
64	13, 62, 63	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩) = (𝐴 ↾ (0..^((#‘𝐴) − 1))))
65	64	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝜑 → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = (#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))))
66		swrd0len 13422	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((#‘𝐴) − 1) ∈ (0...(#‘𝐴))) → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = ((#‘𝐴) − 1))
67	13, 62, 66	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = ((#‘𝐴) − 1))
68	65, 67	eqtr3d 2658	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = ((#‘𝐴) − 1))
69	68	oveq1d 6665	. . . . . . . 8 ⊢ (𝜑 → ((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1) = (((#‘𝐴) − 1) − 1))
70	69	fveq2d 6195	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1)) = ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘(((#‘𝐴) − 1) − 1)))
71		fzo0end 12560	. . . . . . . 8 ⊢ (((#‘𝐴) − 1) ∈ ℕ → (((#‘𝐴) − 1) − 1) ∈ (0..^((#‘𝐴) − 1)))
72		fvres 6207	. . . . . . . 8 ⊢ ((((#‘𝐴) − 1) − 1) ∈ (0..^((#‘𝐴) − 1)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘(((#‘𝐴) − 1) − 1)) = (𝐴‘(((#‘𝐴) − 1) − 1)))
73	21, 71, 72	3syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘(((#‘𝐴) − 1) − 1)) = (𝐴‘(((#‘𝐴) − 1) − 1)))
74	58, 70, 73	3eqtrd 2660	. . . . . 6 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝐴‘(((#‘𝐴) − 1) − 1)))
75	74	fveq2d 6195	. . . . 5 ⊢ (𝜑 → (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) = (#‘(𝐴‘(((#‘𝐴) − 1) − 1))))
76	1, 5, 6, 7, 8, 9	efgsdmi 18145	. . . . . . 7 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((#‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))))
77	4, 21, 76	syl2anc 693	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))))
78	1, 5, 6, 7	efgtlen 18139	. . . . . 6 ⊢ (((𝐴‘(((#‘𝐴) − 1) − 1)) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))) → (#‘(𝑆‘𝐴)) = ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
79	42, 77, 78	syl2anc 693	. . . . 5 ⊢ (𝜑 → (#‘(𝑆‘𝐴)) = ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
80	49, 75, 79	3brtr4d 4685	. . . 4 ⊢ (𝜑 → (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)))
81	1, 5, 6, 7	efgtf 18135	. . . . . . . . . . . 12 ⊢ ((𝐴‘(((#‘𝐴) − 1) − 1)) ∈ 𝑊 → ((𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) = (𝑎 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2_𝑜) ↦ ((𝐴‘(((#‘𝐴) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))):((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊))
82	42, 81	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) = (𝑎 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2_𝑜) ↦ ((𝐴‘(((#‘𝐴) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))):((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊))
83	82	simprd 479	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))):((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊)
84		ffn 6045	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))):((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊 → (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) Fn ((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜)))
85		ovelrn 6810	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) Fn ((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜)) → ((𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) ↔ ∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟)))
86	83, 84, 85	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) ↔ ∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟)))
87	77, 86	mpbid 222	. . . . . . . 8 ⊢ (𝜑 → ∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟))
88	20	simprd 479	. . . . . . . . . 10 ⊢ (𝜑 → ((#‘𝐵) − 1) ∈ ℕ)
89	1, 5, 6, 7, 8, 9	efgsdmi 18145	. . . . . . . . . 10 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((#‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))))
90	17, 88, 89	syl2anc 693	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))))
91	1, 5, 6, 7, 8, 9	efgsdm 18143	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1)))))
92	91	simp1bi 1076	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
93	17, 92	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
94	93	eldifad 3586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ Word 𝑊)
95		wrdf 13310	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(#‘𝐵))⟶𝑊)
96	94, 95	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵:(0..^(#‘𝐵))⟶𝑊)
97		fzo0end 12560	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐵) − 1) ∈ ℕ → (((#‘𝐵) − 1) − 1) ∈ (0..^((#‘𝐵) − 1)))
98		elfzofz 12485	. . . . . . . . . . . . . . 15 ⊢ ((((#‘𝐵) − 1) − 1) ∈ (0..^((#‘𝐵) − 1)) → (((#‘𝐵) − 1) − 1) ∈ (0...((#‘𝐵) − 1)))
99	88, 97, 98	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((#‘𝐵) − 1) − 1) ∈ (0...((#‘𝐵) − 1)))
100		lencl 13324	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ Word 𝑊 → (#‘𝐵) ∈ ℕ₀)
101	94, 100	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (#‘𝐵) ∈ ℕ₀)
102	101	nn0zd 11480	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (#‘𝐵) ∈ ℤ)
103		fzoval 12471	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝐵) ∈ ℤ → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1)))
104	102, 103	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1)))
105	99, 104	eleqtrrd 2704	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((#‘𝐵) − 1) − 1) ∈ (0..^(#‘𝐵)))
106	96, 105	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘(((#‘𝐵) − 1) − 1)) ∈ 𝑊)
107	1, 5, 6, 7	efgtf 18135	. . . . . . . . . . . 12 ⊢ ((𝐵‘(((#‘𝐵) − 1) − 1)) ∈ 𝑊 → ((𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) = (𝑎 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2_𝑜) ↦ ((𝐵‘(((#‘𝐵) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))):((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊))
108	106, 107	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) = (𝑎 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2_𝑜) ↦ ((𝐵‘(((#‘𝐵) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))):((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊))
109	108	simprd 479	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))):((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊)
110		ffn 6045	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))):((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊 → (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) Fn ((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜)))
111		ovelrn 6810	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) Fn ((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜)) → ((𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) ↔ ∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))
112	109, 110, 111	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) ↔ ∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))
113	90, 112	mpbid 222	. . . . . . . 8 ⊢ (𝜑 → ∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠))
114		reeanv 3107	. . . . . . . . 9 ⊢ (∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))
115		reeanv 3107	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (𝐼 × 2_𝑜)∃𝑠 ∈ (𝐼 × 2_𝑜)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))
116	16	ad3antrrr 766	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
117	4	ad3antrrr 766	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝐴 ∈ dom 𝑆)
118	17	ad3antrrr 766	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝐵 ∈ dom 𝑆)
119	18	ad3antrrr 766	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑆‘𝐵))
120	19	ad3antrrr 766	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ¬ (𝐴‘0) = (𝐵‘0))
121		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐴) − 1) − 1) = (((#‘𝐴) − 1) − 1)
122		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐵) − 1) − 1) = (((#‘𝐵) − 1) − 1)
123		simpllr 799	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))))
124	123	simpld 475	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))))
125	123	simprd 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))
126		simplrl 800	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)))
127	126	simpld 475	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝑟 ∈ (𝐼 × 2_𝑜))
128	126	simprd 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝑠 ∈ (𝐼 × 2_𝑜))
129		simplrr 801	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))
130	129	simpld 475	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟))
131	129	simprd 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠))
132		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
133	1, 5, 6, 7, 8, 9, 116, 117, 118, 119, 120, 121, 122, 124, 125, 127, 128, 130, 131, 132	efgredlemb 18159	. . . . . . . . . . . . . 14 ⊢ ¬ (((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
134		iman 440	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) ↔ ¬ (((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
135	133, 134	mpbir 221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
136	135	expr 643	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ (𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜))) → (((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
137	136	rexlimdvva 3038	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) → (∃𝑟 ∈ (𝐼 × 2_𝑜)∃𝑠 ∈ (𝐼 × 2_𝑜)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
138	115, 137	syl5bir 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) → ((∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
139	138	rexlimdvva 3038	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
140	114, 139	syl5bir 233	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
141	87, 113, 140	mp2and 715	. . . . . . 7 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
142		fvres 6207	. . . . . . . 8 ⊢ ((((#‘𝐵) − 1) − 1) ∈ (0..^((#‘𝐵) − 1)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘(((#‘𝐵) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
143	88, 97, 142	3syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘(((#‘𝐵) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
144	141, 73, 143	3eqtr4d 2666	. . . . . 6 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘(((#‘𝐴) − 1) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘(((#‘𝐵) − 1) − 1)))
145		fzss1 12380	. . . . . . . . . . . . 13 ⊢ (1 ∈ (ℤ_≥‘0) → (1...(#‘𝐵)) ⊆ (0...(#‘𝐵)))
146	59, 145	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1...(#‘𝐵)) ⊆ (0...(#‘𝐵))
147	101	nn0red 11352	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (#‘𝐵) ∈ ℝ)
148	147	lem1d 10957	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐵) − 1) ≤ (#‘𝐵))
149		fznn 12408	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐵) ∈ ℤ → (((#‘𝐵) − 1) ∈ (1...(#‘𝐵)) ↔ (((#‘𝐵) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ≤ (#‘𝐵))))
150	102, 149	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((#‘𝐵) − 1) ∈ (1...(#‘𝐵)) ↔ (((#‘𝐵) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ≤ (#‘𝐵))))
151	88, 148, 150	mpbir2and 957	. . . . . . . . . . . 12 ⊢ (𝜑 → ((#‘𝐵) − 1) ∈ (1...(#‘𝐵)))
152	146, 151	sseldi 3601	. . . . . . . . . . 11 ⊢ (𝜑 → ((#‘𝐵) − 1) ∈ (0...(#‘𝐵)))
153		swrd0val 13421	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((#‘𝐵) − 1) ∈ (0...(#‘𝐵))) → (𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩) = (𝐵 ↾ (0..^((#‘𝐵) − 1))))
154	94, 152, 153	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩) = (𝐵 ↾ (0..^((#‘𝐵) − 1))))
155	154	fveq2d 6195	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = (#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
156		swrd0len 13422	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((#‘𝐵) − 1) ∈ (0...(#‘𝐵))) → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = ((#‘𝐵) − 1))
157	94, 152, 156	syl2anc 693	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = ((#‘𝐵) − 1))
158	155, 157	eqtr3d 2658	. . . . . . . 8 ⊢ (𝜑 → (#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = ((#‘𝐵) − 1))
159	158	oveq1d 6665	. . . . . . 7 ⊢ (𝜑 → ((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1) = (((#‘𝐵) − 1) − 1))
160	159	fveq2d 6195	. . . . . 6 ⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘(((#‘𝐵) − 1) − 1)))
161	144, 70, 160	3eqtr4d 2666	. . . . 5 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)))
162	1, 5, 6, 7, 8, 9	efgsres 18151	. . . . . . 7 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((#‘𝐵) − 1) ∈ (1...(#‘𝐵))) → (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆)
163	17, 151, 162	syl2anc 693	. . . . . 6 ⊢ (𝜑 → (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆)
164	1, 5, 6, 7, 8, 9	efgsval 18144	. . . . . 6 ⊢ ((𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆 → (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)))
165	163, 164	syl 17	. . . . 5 ⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)))
166	161, 58, 165	3eqtr4d 2666	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
167		fveq2 6191	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))))
168	167	fveq2d 6195	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (#‘(𝑆‘𝑎)) = (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))))
169	168	breq1d 4663	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) ↔ (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴))))
170	167	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏)))
171		fveq1 6190	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0))
172	171	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0)))
173	170, 172	imbi12d 334	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0))))
174	169, 173	imbi12d 334	. . . . . 6 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0)))))
175		fveq2 6191	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (𝑆‘𝑏) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
176	175	eqeq2d 2632	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))))
177		fveq1 6190	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))
178	177	eqeq2d 2632	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0)))
179	176, 178	imbi12d 334	. . . . . . 7 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))))
180	179	imbi2d 330	. . . . . 6 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0)))))
181	174, 180	rspc2va 3323	. . . . 5 ⊢ ((((𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆 ∧ (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) → ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))))
182	56, 163, 16, 181	syl21anc 1325	. . . 4 ⊢ (𝜑 → ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))))
183	80, 166, 182	mp2d 49	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))
184		lbfzo0 12507	. . . . 5 ⊢ (0 ∈ (0..^((#‘𝐴) − 1)) ↔ ((#‘𝐴) − 1) ∈ ℕ)
185	21, 184	sylibr 224	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((#‘𝐴) − 1)))
186		fvres 6207	. . . 4 ⊢ (0 ∈ (0..^((#‘𝐴) − 1)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝐴‘0))
187	185, 186	syl 17	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝐴‘0))
188		lbfzo0 12507	. . . . 5 ⊢ (0 ∈ (0..^((#‘𝐵) − 1)) ↔ ((#‘𝐵) − 1) ∈ ℕ)
189	88, 188	sylibr 224	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((#‘𝐵) − 1)))
190		fvres 6207	. . . 4 ⊢ (0 ∈ (0..^((#‘𝐵) − 1)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝐵‘0))
191	189, 190	syl 17	. . 3 ⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝐵‘0))
192	183, 187, 191	3eqtr3d 2664	. 2 ⊢ (𝜑 → (𝐴‘0) = (𝐵‘0))
193	192, 19	pm2.65i 185	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 {crab 2916 ∖ cdif 3571 ⊆ wss 3574 ∅c0 3915 {csn 4177 ⟨cop 4183 ⟨cotp 4185 ∪ ciun 4520 class class class wbr 4653 ↦ cmpt 4729 I cid 5023 × cxp 5112 dom cdm 5114 ran crn 5115 ↾ cres 5116 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 1_𝑜c1o 7553 2_𝑜c2o 7554 Fincfn 7955 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 < clt 10074 ≤ cle 10075 − cmin 10266 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 ...cfz 12326 ..^cfzo 12465 #chash 13117 Word cword 13291 substr csubstr 13295 splice csplice 13296 ⟨“cs2 13586 ~_FG cefg 18119

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-ot 4186 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-concat 13301 df-s1 13302 df-substr 13303 df-splice 13304 df-s2 13593

This theorem is referenced by: efgred 18161

W3C validator