swrdf1 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > swrdf1		Structured version Visualization version GIF version

Theorem swrdf1 33285

Description: Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-Dec-2023.)

**Hypotheses**
Ref	Expression
swrdf1.w	⊢ (𝜑 → 𝑊 ∈ Word 𝐷)
swrdf1.m	⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
swrdf1.n	⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝑊)))
swrdf1.1	⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)

**Assertion**
Ref	Expression
swrdf1	⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)–1-1→𝐷)

Proof of Theorem swrdf1 Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		swrdf1.w	. . . 4 ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)
2		swrdf1.m	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
3		swrdf1.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝑊)))
4		swrdf 14695	. . . 4 ⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝑀, 𝑁⟩):(0..^(𝑁 − 𝑀))⟶𝐷)
5	1, 2, 3, 4	syl3anc 1397	. . 3 ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):(0..^(𝑁 − 𝑀))⟶𝐷)
6	5	ffdmd 6736	. 2 ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)⟶𝐷)
7		fzossz 13715	. . . . . . . 8 ⊢ (0..^(𝑁 − 𝑀)) ⊆ ℤ
8		simpllr 787	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩))
9	5	fdmd 6716	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑊 substr ⟨𝑀, 𝑁⟩) = (0..^(𝑁 − 𝑀)))
10	9	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → dom (𝑊 substr ⟨𝑀, 𝑁⟩) = (0..^(𝑁 − 𝑀)))
11	8, 10	eleqtrd 2864	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 ∈ (0..^(𝑁 − 𝑀)))
12	7, 11	sselid 3934	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 ∈ ℤ)
13	12	zcnd 12707	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 ∈ ℂ)
14		simplr 780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩))
15	14, 10	eleqtrd 2864	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑗 ∈ (0..^(𝑁 − 𝑀)))
16	7, 15	sselid 3934	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑗 ∈ ℤ)
17	16	zcnd 12707	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑗 ∈ ℂ)
18	2	elfzelzd 13559	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑀 ∈ ℤ)
20	19	zcnd 12707	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑀 ∈ ℂ)
21		swrdf1.1	. . . . . . . 8 ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)
22	21	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑊:dom 𝑊–1-1→𝐷)
23		elfzuz 13554	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ (ℤ_≥‘0))
24		fzoss1 13722	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ_≥‘0) → (𝑀..^𝑁) ⊆ (0..^𝑁))
25	2, 23, 24	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀..^𝑁) ⊆ (0..^𝑁))
26		elfzuz3 13555	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (0...(♯‘𝑊)) → (♯‘𝑊) ∈ (ℤ_≥‘𝑁))
27		fzoss2 13723	. . . . . . . . . . . 12 ⊢ ((♯‘𝑊) ∈ (ℤ_≥‘𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝑊)))
28	3, 26, 27	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(♯‘𝑊)))
29	25, 28	sstrd 3946	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀..^𝑁) ⊆ (0..^(♯‘𝑊)))
30	29	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑀..^𝑁) ⊆ (0..^(♯‘𝑊)))
31	3	elfzelzd 13559	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
32	31	ad3antrrr 742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑁 ∈ ℤ)
33		fzoaddel2 13756	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 + 𝑀) ∈ (𝑀..^𝑁))
34	11, 32, 19, 33	syl3anc 1397	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑖 + 𝑀) ∈ (𝑀..^𝑁))
35	30, 34	sseldd 3937	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊)))
36		wrddm 14565	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊)))
37	1, 36	syl 18	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
38	37	ad3antrrr 742	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → dom 𝑊 = (0..^(♯‘𝑊)))
39	35, 38	eleqtrrd 2865	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑖 + 𝑀) ∈ dom 𝑊)
40		fzoaddel2 13756	. . . . . . . . . 10 ⊢ ((𝑗 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 + 𝑀) ∈ (𝑀..^𝑁))
41	15, 32, 19, 40	syl3anc 1397	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑗 + 𝑀) ∈ (𝑀..^𝑁))
42	30, 41	sseldd 3937	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑗 + 𝑀) ∈ (0..^(♯‘𝑊)))
43	42, 38	eleqtrrd 2865	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑗 + 𝑀) ∈ dom 𝑊)
44		simpr 489	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗))
45	1	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑊 ∈ Word 𝐷)
46	2	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑀 ∈ (0...𝑁))
47	3	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑁 ∈ (0...(♯‘𝑊)))
48		swrdfv 14693	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = (𝑊‘(𝑖 + 𝑀)))
49	45, 46, 47, 11, 48	syl31anc 1399	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = (𝑊‘(𝑖 + 𝑀)))
50		swrdfv 14693	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = (𝑊‘(𝑗 + 𝑀)))
51	45, 46, 47, 15, 50	syl31anc 1399	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = (𝑊‘(𝑗 + 𝑀)))
52	44, 49, 51	3eqtr3d 2805	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑊‘(𝑖 + 𝑀)) = (𝑊‘(𝑗 + 𝑀)))
53		f1veqaeq 7254	. . . . . . . . 9 ⊢ ((𝑊:dom 𝑊–1-1→𝐷 ∧ ((𝑖 + 𝑀) ∈ dom 𝑊 ∧ (𝑗 + 𝑀) ∈ dom 𝑊)) → ((𝑊‘(𝑖 + 𝑀)) = (𝑊‘(𝑗 + 𝑀)) → (𝑖 + 𝑀) = (𝑗 + 𝑀)))
54	53	anassrs 472	. . . . . . . 8 ⊢ (((𝑊:dom 𝑊–1-1→𝐷 ∧ (𝑖 + 𝑀) ∈ dom 𝑊) ∧ (𝑗 + 𝑀) ∈ dom 𝑊) → ((𝑊‘(𝑖 + 𝑀)) = (𝑊‘(𝑗 + 𝑀)) → (𝑖 + 𝑀) = (𝑗 + 𝑀)))
55	54	imp 411	. . . . . . 7 ⊢ ((((𝑊:dom 𝑊–1-1→𝐷 ∧ (𝑖 + 𝑀) ∈ dom 𝑊) ∧ (𝑗 + 𝑀) ∈ dom 𝑊) ∧ (𝑊‘(𝑖 + 𝑀)) = (𝑊‘(𝑗 + 𝑀))) → (𝑖 + 𝑀) = (𝑗 + 𝑀))
56	22, 39, 43, 52, 55	syl1111anc 853	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑖 + 𝑀) = (𝑗 + 𝑀))
57	13, 17, 20, 56	addcan2ad 11422	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 = 𝑗)
58	57	ex 417	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) → (((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) → 𝑖 = 𝑗))
59	58	anasss 471	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩))) → (((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) → 𝑖 = 𝑗))
60	59	ralrimivva 3207	. 2 ⊢ (𝜑 → ∀𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)∀𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)(((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) → 𝑖 = 𝑗))
61		dff13 7252	. 2 ⊢ ((𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)–1-1→𝐷 ↔ ((𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)⟶𝐷 ∧ ∀𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)∀𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)(((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) → 𝑖 = 𝑗)))
62	6, 60, 61	sylanbrc 594	1 ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)–1-1→𝐷)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 = wceq 1569 ∈ wcel 2142 ∀wral 3078 ⊆ wss 3904 ⟨cop 4594 dom cdm 5660 ⟶wf 6532 –1-1→wf1 6533 ‘cfv 6536 (class class class)co 7412 0cc0 11106 + caddc 11109 − cmin 11447 ℤcz 12597 ℤ_≥cuz 12868 ...cfz 13541 ..^cfzo 13689 ♯chash 14373 Word cword 14557 substr csubstr 14685

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-nn 12240 df-n0 12511 df-z 12598 df-uz 12869 df-fz 13542 df-fzo 13690 df-hash 14374 df-word 14558 df-substr 14686

This theorem is used by: cycpmco2f1 33453

W3C validator