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 17983

Description: The reduced word that forms the base of the sequence in efgsval 17967 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 6166	. . . . . . . . . 10 ⊢ ( I ‘Word (𝐼 × 2_𝑜)) ⊆ Word (𝐼 × 2_𝑜)
3	1, 2	eqsstri 3598	. . . . . . . . 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 17966	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1)))))
11	10	simp1bi 1069	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
12	4, 11	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
13	12	eldifad 3552	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ Word 𝑊)
14		wrdf 13165	. . . . . . . . . . 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 17976	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ∈ ℕ))
21	20	simpld 474	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ ℕ)
22		nnm1nn0 11211	. . . . . . . . . . . . 13 ⊢ (((#‘𝐴) − 1) ∈ ℕ → (((#‘𝐴) − 1) − 1) ∈ ℕ₀)
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ ℕ₀)
24	21	nnred 10912	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ ℝ)
25	24	lem1d 10836	. . . . . . . . . . . 12 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ≤ ((#‘𝐴) − 1))
26		eldifsni 4261	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ≠ ∅)
27	4, 11, 26	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ ∅)
28		wrdfin 13178	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑊 → 𝐴 ∈ Fin)
29		hashnncl 13018	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
30	13, 28, 29	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
31	27, 30	mpbird 246	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ)
32		nnm1nn0 11211	. . . . . . . . . . . . 13 ⊢ ((#‘𝐴) ∈ ℕ → ((#‘𝐴) − 1) ∈ ℕ₀)
33		fznn0 12301	. . . . . . . . . . . . 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 959	. . . . . . . . . . 11 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ (0...((#‘𝐴) − 1)))
36		lencl 13179	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Word 𝑊 → (#‘𝐴) ∈ ℕ₀)
37	13, 36	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ₀)
38	37	nn0zd 11356	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐴) ∈ ℤ)
39		fzoval 12340	. . . . . . . . . . . 12 ⊢ ((#‘𝐴) ∈ ℤ → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1)))
40	38, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1)))
41	35, 40	eleqtrrd 2691	. . . . . . . . . 10 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ (0..^(#‘𝐴)))
42	15, 41	ffvelrnd 6268	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) ∈ 𝑊)
43	3, 42	sseldi 3566	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2_𝑜))
44		lencl 13179	. . . . . . . 8 ⊢ ((𝐴‘(((#‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2_𝑜) → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℕ₀)
45	43, 44	syl 17	. . . . . . 7 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℕ₀)
46	45	nn0red 11229	. . . . . 6 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℝ)
47		2rp 11713	. . . . . 6 ⊢ 2 ∈ ℝ⁺
48		ltaddrp 11743	. . . . . 6 ⊢ (((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℝ ∧ 2 ∈ ℝ⁺) → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) < ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
49	46, 47, 48	sylancl 693	. . . . 5 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) < ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
50	37	nn0red 11229	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝐴) ∈ ℝ)
51	50	lem1d 10836	. . . . . . . . . 10 ⊢ (𝜑 → ((#‘𝐴) − 1) ≤ (#‘𝐴))
52		fznn 12278	. . . . . . . . . . 11 ⊢ ((#‘𝐴) ∈ ℤ → (((#‘𝐴) − 1) ∈ (1...(#‘𝐴)) ↔ (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐴) − 1) ≤ (#‘𝐴))))
53	38, 52	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (((#‘𝐴) − 1) ∈ (1...(#‘𝐴)) ↔ (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐴) − 1) ≤ (#‘𝐴))))
54	21, 51, 53	mpbir2and 959	. . . . . . . . 9 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ (1...(#‘𝐴)))
55	1, 5, 6, 7, 8, 9	efgsres 17974	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((#‘𝐴) − 1) ∈ (1...(#‘𝐴))) → (𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆)
56	4, 54, 55	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆)
57	1, 5, 6, 7, 8, 9	efgsval 17967	. . . . . . . 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 11608	. . . . . . . . . . . . . 14 ⊢ 1 ∈ (ℤ_≥‘0)
60		fzss1 12251	. . . . . . . . . . . . . 14 ⊢ (1 ∈ (ℤ_≥‘0) → (1...(#‘𝐴)) ⊆ (0...(#‘𝐴)))
61	59, 60	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1...(#‘𝐴)) ⊆ (0...(#‘𝐴))
62	61, 54	sseldi 3566	. . . . . . . . . . . 12 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ (0...(#‘𝐴)))
63		swrd0val 13273	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((#‘𝐴) − 1) ∈ (0...(#‘𝐴))) → (𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩) = (𝐴 ↾ (0..^((#‘𝐴) − 1))))
64	13, 62, 63	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩) = (𝐴 ↾ (0..^((#‘𝐴) − 1))))
65	64	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜑 → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = (#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))))
66		swrd0len 13274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((#‘𝐴) − 1) ∈ (0...(#‘𝐴))) → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = ((#‘𝐴) − 1))
67	13, 62, 66	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = ((#‘𝐴) − 1))
68	65, 67	eqtr3d 2646	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = ((#‘𝐴) − 1))
69	68	oveq1d 6564	. . . . . . . 8 ⊢ (𝜑 → ((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1) = (((#‘𝐴) − 1) − 1))
70	69	fveq2d 6107	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1)) = ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘(((#‘𝐴) − 1) − 1)))
71		fzo0end 12426	. . . . . . . 8 ⊢ (((#‘𝐴) − 1) ∈ ℕ → (((#‘𝐴) − 1) − 1) ∈ (0..^((#‘𝐴) − 1)))
72		fvres 6117	. . . . . . . 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 2648	. . . . . 6 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝐴‘(((#‘𝐴) − 1) − 1)))
75	74	fveq2d 6107	. . . . 5 ⊢ (𝜑 → (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) = (#‘(𝐴‘(((#‘𝐴) − 1) − 1))))
76	1, 5, 6, 7, 8, 9	efgsdmi 17968	. . . . . . 7 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((#‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))))
77	4, 21, 76	syl2anc 691	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))))
78	1, 5, 6, 7	efgtlen 17962	. . . . . 6 ⊢ (((𝐴‘(((#‘𝐴) − 1) − 1)) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))) → (#‘(𝑆‘𝐴)) = ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
79	42, 77, 78	syl2anc 691	. . . . 5 ⊢ (𝜑 → (#‘(𝑆‘𝐴)) = ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
80	49, 75, 79	3brtr4d 4615	. . . 4 ⊢ (𝜑 → (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)))
81	1, 5, 6, 7	efgtf 17958	. . . . . . . . . . . 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 478	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))):((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊)
84		ffn 5958	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))):((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊 → (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) Fn ((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜)))
85		ovelrn 6708	. . . . . . . . . 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 221	. . . . . . . 8 ⊢ (𝜑 → ∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟))
88	20	simprd 478	. . . . . . . . . 10 ⊢ (𝜑 → ((#‘𝐵) − 1) ∈ ℕ)
89	1, 5, 6, 7, 8, 9	efgsdmi 17968	. . . . . . . . . 10 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((#‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))))
90	17, 88, 89	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))))
91	1, 5, 6, 7, 8, 9	efgsdm 17966	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1)))))
92	91	simp1bi 1069	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
93	17, 92	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
94	93	eldifad 3552	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ Word 𝑊)
95		wrdf 13165	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(#‘𝐵))⟶𝑊)
96	94, 95	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵:(0..^(#‘𝐵))⟶𝑊)
97		fzo0end 12426	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐵) − 1) ∈ ℕ → (((#‘𝐵) − 1) − 1) ∈ (0..^((#‘𝐵) − 1)))
98		elfzofz 12354	. . . . . . . . . . . . . . 15 ⊢ ((((#‘𝐵) − 1) − 1) ∈ (0..^((#‘𝐵) − 1)) → (((#‘𝐵) − 1) − 1) ∈ (0...((#‘𝐵) − 1)))
99	88, 97, 98	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((#‘𝐵) − 1) − 1) ∈ (0...((#‘𝐵) − 1)))
100		lencl 13179	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ Word 𝑊 → (#‘𝐵) ∈ ℕ₀)
101	94, 100	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (#‘𝐵) ∈ ℕ₀)
102	101	nn0zd 11356	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (#‘𝐵) ∈ ℤ)
103		fzoval 12340	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝐵) ∈ ℤ → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1)))
104	102, 103	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1)))
105	99, 104	eleqtrrd 2691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((#‘𝐵) − 1) − 1) ∈ (0..^(#‘𝐵)))
106	96, 105	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘(((#‘𝐵) − 1) − 1)) ∈ 𝑊)
107	1, 5, 6, 7	efgtf 17958	. . . . . . . . . . . 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 478	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))):((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊)
110		ffn 5958	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))):((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊 → (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) Fn ((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜)))
111		ovelrn 6708	. . . . . . . . . 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 221	. . . . . . . 8 ⊢ (𝜑 → ∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠))
114		reeanv 3086	. . . . . . . . 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 3086	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (𝐼 × 2_𝑜)∃𝑠 ∈ (𝐼 × 2_𝑜)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))
116	16	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
117	4	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝐴 ∈ dom 𝑆)
118	17	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝐵 ∈ dom 𝑆)
119	18	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑆‘𝐵))
120	19	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ¬ (𝐴‘0) = (𝐵‘0))
121		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐴) − 1) − 1) = (((#‘𝐴) − 1) − 1)
122		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐵) − 1) − 1) = (((#‘𝐵) − 1) − 1)
123		simpllr 795	. . . . . . . . . . . . . . . 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 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))))
125	123	simprd 478	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))
126		simplrl 796	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)))
127	126	simpld 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝑟 ∈ (𝐼 × 2_𝑜))
128	126	simprd 478	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝑠 ∈ (𝐼 × 2_𝑜))
129		simplrr 797	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))
130	129	simpld 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟))
131	129	simprd 478	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠))
132		simpr 476	. . . . . . . . . . . . . . 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 17982	. . . . . . . . . . . . . 14 ⊢ ¬ (((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
134		iman 439	. . . . . . . . . . . . . 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 220	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
136	135	expr 641	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ (𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜))) → (((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
137	136	rexlimdvva 3020	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) → (∃𝑟 ∈ (𝐼 × 2_𝑜)∃𝑠 ∈ (𝐼 × 2_𝑜)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
138	115, 137	syl5bir 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) → ((∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
139	138	rexlimdvva 3020	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
140	114, 139	syl5bir 232	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
141	87, 113, 140	mp2and 711	. . . . . . 7 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
142		fvres 6117	. . . . . . . 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 2654	. . . . . 6 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘(((#‘𝐴) − 1) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘(((#‘𝐵) − 1) − 1)))
145		fzss1 12251	. . . . . . . . . . . . 13 ⊢ (1 ∈ (ℤ_≥‘0) → (1...(#‘𝐵)) ⊆ (0...(#‘𝐵)))
146	59, 145	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1...(#‘𝐵)) ⊆ (0...(#‘𝐵))
147	101	nn0red 11229	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (#‘𝐵) ∈ ℝ)
148	147	lem1d 10836	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐵) − 1) ≤ (#‘𝐵))
149		fznn 12278	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐵) ∈ ℤ → (((#‘𝐵) − 1) ∈ (1...(#‘𝐵)) ↔ (((#‘𝐵) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ≤ (#‘𝐵))))
150	102, 149	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((#‘𝐵) − 1) ∈ (1...(#‘𝐵)) ↔ (((#‘𝐵) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ≤ (#‘𝐵))))
151	88, 148, 150	mpbir2and 959	. . . . . . . . . . . 12 ⊢ (𝜑 → ((#‘𝐵) − 1) ∈ (1...(#‘𝐵)))
152	146, 151	sseldi 3566	. . . . . . . . . . 11 ⊢ (𝜑 → ((#‘𝐵) − 1) ∈ (0...(#‘𝐵)))
153		swrd0val 13273	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((#‘𝐵) − 1) ∈ (0...(#‘𝐵))) → (𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩) = (𝐵 ↾ (0..^((#‘𝐵) − 1))))
154	94, 152, 153	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩) = (𝐵 ↾ (0..^((#‘𝐵) − 1))))
155	154	fveq2d 6107	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = (#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
156		swrd0len 13274	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((#‘𝐵) − 1) ∈ (0...(#‘𝐵))) → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = ((#‘𝐵) − 1))
157	94, 152, 156	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = ((#‘𝐵) − 1))
158	155, 157	eqtr3d 2646	. . . . . . . 8 ⊢ (𝜑 → (#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = ((#‘𝐵) − 1))
159	158	oveq1d 6564	. . . . . . 7 ⊢ (𝜑 → ((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1) = (((#‘𝐵) − 1) − 1))
160	159	fveq2d 6107	. . . . . 6 ⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘(((#‘𝐵) − 1) − 1)))
161	144, 70, 160	3eqtr4d 2654	. . . . 5 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)))
162	1, 5, 6, 7, 8, 9	efgsres 17974	. . . . . . 7 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((#‘𝐵) − 1) ∈ (1...(#‘𝐵))) → (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆)
163	17, 151, 162	syl2anc 691	. . . . . 6 ⊢ (𝜑 → (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆)
164	1, 5, 6, 7, 8, 9	efgsval 17967	. . . . . 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 2654	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
167		fveq2 6103	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))))
168	167	fveq2d 6107	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (#‘(𝑆‘𝑎)) = (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))))
169	168	breq1d 4593	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) ↔ (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴))))
170	167	eqeq1d 2612	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏)))
171		fveq1 6102	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0))
172	171	eqeq1d 2612	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0)))
173	170, 172	imbi12d 333	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0))))
174	169, 173	imbi12d 333	. . . . . 6 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0)))))
175		fveq2 6103	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (𝑆‘𝑏) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
176	175	eqeq2d 2620	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))))
177		fveq1 6102	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))
178	177	eqeq2d 2620	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0)))
179	176, 178	imbi12d 333	. . . . . . 7 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))))
180	179	imbi2d 329	. . . . . 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 3294	. . . . 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 1317	. . . 4 ⊢ (𝜑 → ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))))
183	80, 166, 182	mp2d 47	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))
184		lbfzo0 12375	. . . . 5 ⊢ (0 ∈ (0..^((#‘𝐴) − 1)) ↔ ((#‘𝐴) − 1) ∈ ℕ)
185	21, 184	sylibr 223	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((#‘𝐴) − 1)))
186		fvres 6117	. . . 4 ⊢ (0 ∈ (0..^((#‘𝐴) − 1)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝐴‘0))
187	185, 186	syl 17	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝐴‘0))
188		lbfzo0 12375	. . . . 5 ⊢ (0 ∈ (0..^((#‘𝐵) − 1)) ↔ ((#‘𝐵) − 1) ∈ ℕ)
189	88, 188	sylibr 223	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((#‘𝐵) − 1)))
190		fvres 6117	. . . 4 ⊢ (0 ∈ (0..^((#‘𝐵) − 1)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝐵‘0))
191	189, 190	syl 17	. . 3 ⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝐵‘0))
192	183, 187, 191	3eqtr3d 2652	. 2 ⊢ (𝜑 → (𝐴‘0) = (𝐵‘0))
193	192, 19	pm2.65i 184	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 ∖ cdif 3537 ⊆ wss 3540 ∅c0 3874 {csn 4125 ⟨cop 4131 ⟨cotp 4133 ∪ ciun 4455 class class class wbr 4583 ↦ cmpt 4643 I cid 4948 × cxp 5036 dom cdm 5038 ran crn 5039 ↾ cres 5040 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 1_𝑜c1o 7440 2_𝑜c2o 7441 Fincfn 7841 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ℝ⁺crp 11708 ...cfz 12197 ..^cfzo 12334 #chash 12979 Word cword 13146 substr csubstr 13150 splice csplice 13151 ⟨“cs2 13437 ~_FG cefg 17942

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-ot 4134 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-hash 12980 df-word 13154 df-concat 13156 df-s1 13157 df-substr 13158 df-splice 13159 df-s2 13444

This theorem is referenced by: efgred 17984

W3C validator