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 18081

Description: The reduced word that forms the base of the sequence in efgsval 18065 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 6213	. . . . . . . . . 10 ⊢ ( I ‘Word (𝐼 × 2_𝑜)) ⊆ Word (𝐼 × 2_𝑜)
3	1, 2	eqsstri 3614	. . . . . . . . 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 18064	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1)))))
11	10	simp1bi 1074	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
12	4, 11	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅}))
13	12	eldifad 3567	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ Word 𝑊)
14		wrdf 13249	. . . . . . . . . . 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 18074	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ∈ ℕ))
21	20	simpld 475	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ ℕ)
22		nnm1nn0 11278	. . . . . . . . . . . . 13 ⊢ (((#‘𝐴) − 1) ∈ ℕ → (((#‘𝐴) − 1) − 1) ∈ ℕ₀)
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ ℕ₀)
24	21	nnred 10979	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ ℝ)
25	24	lem1d 10901	. . . . . . . . . . . 12 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ≤ ((#‘𝐴) − 1))
26		eldifsni 4289	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ≠ ∅)
27	4, 11, 26	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ ∅)
28		wrdfin 13262	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑊 → 𝐴 ∈ Fin)
29		hashnncl 13097	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
30	13, 28, 29	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
31	27, 30	mpbird 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ)
32		nnm1nn0 11278	. . . . . . . . . . . . 13 ⊢ ((#‘𝐴) ∈ ℕ → ((#‘𝐴) − 1) ∈ ℕ₀)
33		fznn0 12373	. . . . . . . . . . . . 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 956	. . . . . . . . . . 11 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ (0...((#‘𝐴) − 1)))
36		lencl 13263	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Word 𝑊 → (#‘𝐴) ∈ ℕ₀)
37	13, 36	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ₀)
38	37	nn0zd 11424	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐴) ∈ ℤ)
39		fzoval 12412	. . . . . . . . . . . 12 ⊢ ((#‘𝐴) ∈ ℤ → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1)))
40	38, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1)))
41	35, 40	eleqtrrd 2701	. . . . . . . . . 10 ⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈ (0..^(#‘𝐴)))
42	15, 41	ffvelrnd 6316	. . . . . . . . 9 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) ∈ 𝑊)
43	3, 42	sseldi 3581	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2_𝑜))
44		lencl 13263	. . . . . . . 8 ⊢ ((𝐴‘(((#‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2_𝑜) → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℕ₀)
45	43, 44	syl 17	. . . . . . 7 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℕ₀)
46	45	nn0red 11296	. . . . . 6 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℝ)
47		2rp 11781	. . . . . 6 ⊢ 2 ∈ ℝ⁺
48		ltaddrp 11811	. . . . . 6 ⊢ (((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) ∈ ℝ ∧ 2 ∈ ℝ⁺) → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) < ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
49	46, 47, 48	sylancl 693	. . . . 5 ⊢ (𝜑 → (#‘(𝐴‘(((#‘𝐴) − 1) − 1))) < ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
50	37	nn0red 11296	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝐴) ∈ ℝ)
51	50	lem1d 10901	. . . . . . . . . 10 ⊢ (𝜑 → ((#‘𝐴) − 1) ≤ (#‘𝐴))
52		fznn 12350	. . . . . . . . . . 11 ⊢ ((#‘𝐴) ∈ ℤ → (((#‘𝐴) − 1) ∈ (1...(#‘𝐴)) ↔ (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐴) − 1) ≤ (#‘𝐴))))
53	38, 52	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (((#‘𝐴) − 1) ∈ (1...(#‘𝐴)) ↔ (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐴) − 1) ≤ (#‘𝐴))))
54	21, 51, 53	mpbir2and 956	. . . . . . . . 9 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ (1...(#‘𝐴)))
55	1, 5, 6, 7, 8, 9	efgsres 18072	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((#‘𝐴) − 1) ∈ (1...(#‘𝐴))) → (𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆)
56	4, 54, 55	syl2anc 692	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆)
57	1, 5, 6, 7, 8, 9	efgsval 18065	. . . . . . . 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 11676	. . . . . . . . . . . . . 14 ⊢ 1 ∈ (ℤ_≥‘0)
60		fzss1 12322	. . . . . . . . . . . . . 14 ⊢ (1 ∈ (ℤ_≥‘0) → (1...(#‘𝐴)) ⊆ (0...(#‘𝐴)))
61	59, 60	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1...(#‘𝐴)) ⊆ (0...(#‘𝐴))
62	61, 54	sseldi 3581	. . . . . . . . . . . 12 ⊢ (𝜑 → ((#‘𝐴) − 1) ∈ (0...(#‘𝐴)))
63		swrd0val 13359	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((#‘𝐴) − 1) ∈ (0...(#‘𝐴))) → (𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩) = (𝐴 ↾ (0..^((#‘𝐴) − 1))))
64	13, 62, 63	syl2anc 692	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩) = (𝐴 ↾ (0..^((#‘𝐴) − 1))))
65	64	fveq2d 6152	. . . . . . . . . 10 ⊢ (𝜑 → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = (#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))))
66		swrd0len 13360	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑊 ∧ ((#‘𝐴) − 1) ∈ (0...(#‘𝐴))) → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = ((#‘𝐴) − 1))
67	13, 62, 66	syl2anc 692	. . . . . . . . . 10 ⊢ (𝜑 → (#‘(𝐴 substr ⟨0, ((#‘𝐴) − 1)⟩)) = ((#‘𝐴) − 1))
68	65, 67	eqtr3d 2657	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = ((#‘𝐴) − 1))
69	68	oveq1d 6619	. . . . . . . 8 ⊢ (𝜑 → ((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1) = (((#‘𝐴) − 1) − 1))
70	69	fveq2d 6152	. . . . . . 7 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1)) = ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘(((#‘𝐴) − 1) − 1)))
71		fzo0end 12501	. . . . . . . 8 ⊢ (((#‘𝐴) − 1) ∈ ℕ → (((#‘𝐴) − 1) − 1) ∈ (0..^((#‘𝐴) − 1)))
72		fvres 6164	. . . . . . . 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 2659	. . . . . 6 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝐴‘(((#‘𝐴) − 1) − 1)))
75	74	fveq2d 6152	. . . . 5 ⊢ (𝜑 → (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) = (#‘(𝐴‘(((#‘𝐴) − 1) − 1))))
76	1, 5, 6, 7, 8, 9	efgsdmi 18066	. . . . . . 7 ⊢ ((𝐴 ∈ dom 𝑆 ∧ ((#‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))))
77	4, 21, 76	syl2anc 692	. . . . . 6 ⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))))
78	1, 5, 6, 7	efgtlen 18060	. . . . . 6 ⊢ (((𝐴‘(((#‘𝐴) − 1) − 1)) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))) → (#‘(𝑆‘𝐴)) = ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
79	42, 77, 78	syl2anc 692	. . . . 5 ⊢ (𝜑 → (#‘(𝑆‘𝐴)) = ((#‘(𝐴‘(((#‘𝐴) − 1) − 1))) + 2))
80	49, 75, 79	3brtr4d 4645	. . . 4 ⊢ (𝜑 → (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)))
81	1, 5, 6, 7	efgtf 18056	. . . . . . . . . . . 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 6002	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))):((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊 → (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) Fn ((0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) × (𝐼 × 2_𝑜)))
85		ovelrn 6763	. . . . . . . . . 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 18066	. . . . . . . . . 10 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((#‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))))
90	17, 88, 89	syl2anc 692	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))))
91	1, 5, 6, 7, 8, 9	efgsdm 18064	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1)))))
92	91	simp1bi 1074	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
93	17, 92	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅}))
94	93	eldifad 3567	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ Word 𝑊)
95		wrdf 13249	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(#‘𝐵))⟶𝑊)
96	94, 95	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵:(0..^(#‘𝐵))⟶𝑊)
97		fzo0end 12501	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐵) − 1) ∈ ℕ → (((#‘𝐵) − 1) − 1) ∈ (0..^((#‘𝐵) − 1)))
98		elfzofz 12426	. . . . . . . . . . . . . . 15 ⊢ ((((#‘𝐵) − 1) − 1) ∈ (0..^((#‘𝐵) − 1)) → (((#‘𝐵) − 1) − 1) ∈ (0...((#‘𝐵) − 1)))
99	88, 97, 98	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((#‘𝐵) − 1) − 1) ∈ (0...((#‘𝐵) − 1)))
100		lencl 13263	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ Word 𝑊 → (#‘𝐵) ∈ ℕ₀)
101	94, 100	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (#‘𝐵) ∈ ℕ₀)
102	101	nn0zd 11424	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (#‘𝐵) ∈ ℤ)
103		fzoval 12412	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝐵) ∈ ℤ → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1)))
104	102, 103	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1)))
105	99, 104	eleqtrrd 2701	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((#‘𝐵) − 1) − 1) ∈ (0..^(#‘𝐵)))
106	96, 105	ffvelrnd 6316	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵‘(((#‘𝐵) − 1) − 1)) ∈ 𝑊)
107	1, 5, 6, 7	efgtf 18056	. . . . . . . . . . . 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 6002	. . . . . . . . . 10 ⊢ ((𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))):((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜))⟶𝑊 → (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) Fn ((0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))) × (𝐼 × 2_𝑜)))
111		ovelrn 6763	. . . . . . . . . 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 3097	. . . . . . . . 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 3097	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ (𝐼 × 2_𝑜)∃𝑠 ∈ (𝐼 × 2_𝑜)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑟 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2_𝑜)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))
116	16	ad3antrrr 765	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))
117	4	ad3antrrr 765	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝐴 ∈ dom 𝑆)
118	17	ad3antrrr 765	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → 𝐵 ∈ dom 𝑆)
119	18	ad3antrrr 765	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → (𝑆‘𝐴) = (𝑆‘𝐵))
120	19	ad3antrrr 765	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))) → ¬ (𝐴‘0) = (𝐵‘0))
121		eqid 2621	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐴) − 1) − 1) = (((#‘𝐴) − 1) − 1)
122		eqid 2621	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐵) − 1) − 1) = (((#‘𝐵) − 1) − 1)
123		simpllr 798	. . . . . . . . . . . . . . . 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 799	. . . . . . . . . . . . . . . 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 800	. . . . . . . . . . . . . . . 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 18080	. . . . . . . . . . . . . 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 642	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0...(#‘(𝐴‘(((#‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(#‘(𝐵‘(((#‘𝐵) − 1) − 1)))))) ∧ (𝑟 ∈ (𝐼 × 2_𝑜) ∧ 𝑠 ∈ (𝐼 × 2_𝑜))) → (((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1))))
137	136	rexlimdvva 3031	. . . . . . . . . . 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 3031	. . . . . . . . 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 714	. . . . . . 7 ⊢ (𝜑 → (𝐴‘(((#‘𝐴) − 1) − 1)) = (𝐵‘(((#‘𝐵) − 1) − 1)))
142		fvres 6164	. . . . . . . 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 2665	. . . . . 6 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘(((#‘𝐴) − 1) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘(((#‘𝐵) − 1) − 1)))
145		fzss1 12322	. . . . . . . . . . . . 13 ⊢ (1 ∈ (ℤ_≥‘0) → (1...(#‘𝐵)) ⊆ (0...(#‘𝐵)))
146	59, 145	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1...(#‘𝐵)) ⊆ (0...(#‘𝐵))
147	101	nn0red 11296	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (#‘𝐵) ∈ ℝ)
148	147	lem1d 10901	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((#‘𝐵) − 1) ≤ (#‘𝐵))
149		fznn 12350	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐵) ∈ ℤ → (((#‘𝐵) − 1) ∈ (1...(#‘𝐵)) ↔ (((#‘𝐵) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ≤ (#‘𝐵))))
150	102, 149	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((#‘𝐵) − 1) ∈ (1...(#‘𝐵)) ↔ (((#‘𝐵) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ≤ (#‘𝐵))))
151	88, 148, 150	mpbir2and 956	. . . . . . . . . . . 12 ⊢ (𝜑 → ((#‘𝐵) − 1) ∈ (1...(#‘𝐵)))
152	146, 151	sseldi 3581	. . . . . . . . . . 11 ⊢ (𝜑 → ((#‘𝐵) − 1) ∈ (0...(#‘𝐵)))
153		swrd0val 13359	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((#‘𝐵) − 1) ∈ (0...(#‘𝐵))) → (𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩) = (𝐵 ↾ (0..^((#‘𝐵) − 1))))
154	94, 152, 153	syl2anc 692	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩) = (𝐵 ↾ (0..^((#‘𝐵) − 1))))
155	154	fveq2d 6152	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = (#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
156		swrd0len 13360	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑊 ∧ ((#‘𝐵) − 1) ∈ (0...(#‘𝐵))) → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = ((#‘𝐵) − 1))
157	94, 152, 156	syl2anc 692	. . . . . . . . 9 ⊢ (𝜑 → (#‘(𝐵 substr ⟨0, ((#‘𝐵) − 1)⟩)) = ((#‘𝐵) − 1))
158	155, 157	eqtr3d 2657	. . . . . . . 8 ⊢ (𝜑 → (#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = ((#‘𝐵) − 1))
159	158	oveq1d 6619	. . . . . . 7 ⊢ (𝜑 → ((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1) = (((#‘𝐵) − 1) − 1))
160	159	fveq2d 6152	. . . . . 6 ⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘(((#‘𝐵) − 1) − 1)))
161	144, 70, 160	3eqtr4d 2665	. . . . 5 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1)) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)))
162	1, 5, 6, 7, 8, 9	efgsres 18072	. . . . . . 7 ⊢ ((𝐵 ∈ dom 𝑆 ∧ ((#‘𝐵) − 1) ∈ (1...(#‘𝐵))) → (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆)
163	17, 151, 162	syl2anc 692	. . . . . 6 ⊢ (𝜑 → (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆)
164	1, 5, 6, 7, 8, 9	efgsval 18065	. . . . . 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 2665	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
167		fveq2 6148	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))))
168	167	fveq2d 6152	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (#‘(𝑆‘𝑎)) = (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))))
169	168	breq1d 4623	. . . . . . 7 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) ↔ (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴))))
170	167	eqeq1d 2623	. . . . . . . 8 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏)))
171		fveq1 6147	. . . . . . . . 9 ⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0))
172	171	eqeq1d 2623	. . . . . . . 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 6148	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (𝑆‘𝑏) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))
176	175	eqeq2d 2631	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))))
177		fveq1 6147	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0))
178	177	eqeq2d 2631	. . . . . . . 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 3307	. . . . 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 1322	. . . 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 12448	. . . . 5 ⊢ (0 ∈ (0..^((#‘𝐴) − 1)) ↔ ((#‘𝐴) − 1) ∈ ℕ)
185	21, 184	sylibr 224	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((#‘𝐴) − 1)))
186		fvres 6164	. . . 4 ⊢ (0 ∈ (0..^((#‘𝐴) − 1)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝐴‘0))
187	185, 186	syl 17	. . 3 ⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝐴‘0))
188		lbfzo0 12448	. . . . 5 ⊢ (0 ∈ (0..^((#‘𝐵) − 1)) ↔ ((#‘𝐵) − 1) ∈ ℕ)
189	88, 188	sylibr 224	. . . 4 ⊢ (𝜑 → 0 ∈ (0..^((#‘𝐵) − 1)))
190		fvres 6164	. . . 4 ⊢ (0 ∈ (0..^((#‘𝐵) − 1)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝐵‘0))
191	189, 190	syl 17	. . 3 ⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝐵‘0))
192	183, 187, 191	3eqtr3d 2663	. 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 1480 ∈ wcel 1987 ≠ wne 2790 ∀wral 2907 ∃wrex 2908 {crab 2911 ∖ cdif 3552 ⊆ wss 3555 ∅c0 3891 {csn 4148 ⟨cop 4154 ⟨cotp 4156 ∪ ciun 4485 class class class wbr 4613 ↦ cmpt 4673 I cid 4984 × cxp 5072 dom cdm 5074 ran crn 5075 ↾ cres 5076 Fn wfn 5842 ⟶wf 5843 ‘cfv 5847 (class class class)co 6604 ↦ cmpt2 6606 1_𝑜c1o 7498 2_𝑜c2o 7499 Fincfn 7899 ℝcr 9879 0cc0 9880 1c1 9881 + caddc 9883 < clt 10018 ≤ cle 10019 − cmin 10210 ℕcn 10964 2c2 11014 ℕ₀cn0 11236 ℤcz 11321 ℤ_≥cuz 11631 ℝ⁺crp 11776 ...cfz 12268 ..^cfzo 12406 #chash 13057 Word cword 13230 substr csubstr 13234 splice csplice 13235 ⟨“cs2 13523 ~_FG cefg 18040

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4731 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902 ax-cnex 9936 ax-resscn 9937 ax-1cn 9938 ax-icn 9939 ax-addcl 9940 ax-addrcl 9941 ax-mulcl 9942 ax-mulrcl 9943 ax-mulcom 9944 ax-addass 9945 ax-mulass 9946 ax-distr 9947 ax-i2m1 9948 ax-1ne0 9949 ax-1rid 9950 ax-rnegex 9951 ax-rrecex 9952 ax-cnre 9953 ax-pre-lttri 9954 ax-pre-lttrn 9955 ax-pre-ltadd 9956 ax-pre-mulgt0 9957

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2912 df-rex 2913 df-reu 2914 df-rab 2916 df-v 3188 df-sbc 3418 df-csb 3515 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-pss 3571 df-nul 3892 df-if 4059 df-pw 4132 df-sn 4149 df-pr 4151 df-tp 4153 df-op 4155 df-ot 4157 df-uni 4403 df-int 4441 df-iun 4487 df-br 4614 df-opab 4674 df-mpt 4675 df-tr 4713 df-eprel 4985 df-id 4989 df-po 4995 df-so 4996 df-fr 5033 df-we 5035 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-pred 5639 df-ord 5685 df-on 5686 df-lim 5687 df-suc 5688 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854 df-fv 5855 df-riota 6565 df-ov 6607 df-oprab 6608 df-mpt2 6609 df-om 7013 df-1st 7113 df-2nd 7114 df-wrecs 7352 df-recs 7413 df-rdg 7451 df-1o 7505 df-2o 7506 df-oadd 7509 df-er 7687 df-map 7804 df-pm 7805 df-en 7900 df-dom 7901 df-sdom 7902 df-fin 7903 df-card 8709 df-pnf 10020 df-mnf 10021 df-xr 10022 df-ltxr 10023 df-le 10024 df-sub 10212 df-neg 10213 df-nn 10965 df-2 11023 df-n0 11237 df-z 11322 df-uz 11632 df-rp 11777 df-fz 12269 df-fzo 12407 df-hash 13058 df-word 13238 df-concat 13240 df-s1 13241 df-substr 13242 df-splice 13243 df-s2 13530

This theorem is referenced by: efgred 18082

W3C validator