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 32944

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 14560	. . . 4 ⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝑀, 𝑁⟩):(0..^(𝑁 − 𝑀))⟶𝐷)
5	1, 2, 3, 4	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):(0..^(𝑁 − 𝑀))⟶𝐷)
6	5	ffdmd 6686	. 2 ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)⟶𝐷)
7		fzossz 13581	. . . . . . . 8 ⊢ (0..^(𝑁 − 𝑀)) ⊆ ℤ
8		simpllr 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩))
9	5	fdmd 6666	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑊 substr ⟨𝑀, 𝑁⟩) = (0..^(𝑁 − 𝑀)))
10	9	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → dom (𝑊 substr ⟨𝑀, 𝑁⟩) = (0..^(𝑁 − 𝑀)))
11	8, 10	eleqtrd 2835	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 ∈ (0..^(𝑁 − 𝑀)))
12	7, 11	sselid 3928	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 ∈ ℤ)
13	12	zcnd 12584	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 ∈ ℂ)
14		simplr 768	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩))
15	14, 10	eleqtrd 2835	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑗 ∈ (0..^(𝑁 − 𝑀)))
16	7, 15	sselid 3928	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑗 ∈ ℤ)
17	16	zcnd 12584	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑗 ∈ ℂ)
18	2	elfzelzd 13427	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑀 ∈ ℤ)
20	19	zcnd 12584	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑀 ∈ ℂ)
21		swrdf1.1	. . . . . . . 8 ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)
22	21	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑊:dom 𝑊–1-1→𝐷)
23		elfzuz 13422	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ (ℤ_≥‘0))
24		fzoss1 13588	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ_≥‘0) → (𝑀..^𝑁) ⊆ (0..^𝑁))
25	2, 23, 24	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀..^𝑁) ⊆ (0..^𝑁))
26		elfzuz3 13423	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (0...(♯‘𝑊)) → (♯‘𝑊) ∈ (ℤ_≥‘𝑁))
27		fzoss2 13589	. . . . . . . . . . . 12 ⊢ ((♯‘𝑊) ∈ (ℤ_≥‘𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝑊)))
28	3, 26, 27	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(♯‘𝑊)))
29	25, 28	sstrd 3941	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀..^𝑁) ⊆ (0..^(♯‘𝑊)))
30	29	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑀..^𝑁) ⊆ (0..^(♯‘𝑊)))
31	3	elfzelzd 13427	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
32	31	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑁 ∈ ℤ)
33		fzoaddel2 13622	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 + 𝑀) ∈ (𝑀..^𝑁))
34	11, 32, 19, 33	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑖 + 𝑀) ∈ (𝑀..^𝑁))
35	30, 34	sseldd 3931	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑖 + 𝑀) ∈ (0..^(♯‘𝑊)))
36		wrddm 14430	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊)))
37	1, 36	syl 17	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
38	37	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → dom 𝑊 = (0..^(♯‘𝑊)))
39	35, 38	eleqtrrd 2836	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑖 + 𝑀) ∈ dom 𝑊)
40		fzoaddel2 13622	. . . . . . . . . 10 ⊢ ((𝑗 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 + 𝑀) ∈ (𝑀..^𝑁))
41	15, 32, 19, 40	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑗 + 𝑀) ∈ (𝑀..^𝑁))
42	30, 41	sseldd 3931	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑗 + 𝑀) ∈ (0..^(♯‘𝑊)))
43	42, 38	eleqtrrd 2836	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑗 + 𝑀) ∈ dom 𝑊)
44		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗))
45	1	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑊 ∈ Word 𝐷)
46	2	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑀 ∈ (0...𝑁))
47	3	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑁 ∈ (0...(♯‘𝑊)))
48		swrdfv 14558	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = (𝑊‘(𝑖 + 𝑀)))
49	45, 46, 47, 11, 48	syl31anc 1375	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = (𝑊‘(𝑖 + 𝑀)))
50		swrdfv 14558	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝐷 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = (𝑊‘(𝑗 + 𝑀)))
51	45, 46, 47, 15, 50	syl31anc 1375	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = (𝑊‘(𝑗 + 𝑀)))
52	44, 49, 51	3eqtr3d 2776	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑊‘(𝑖 + 𝑀)) = (𝑊‘(𝑗 + 𝑀)))
53		f1veqaeq 7196	. . . . . . . . 9 ⊢ ((𝑊:dom 𝑊–1-1→𝐷 ∧ ((𝑖 + 𝑀) ∈ dom 𝑊 ∧ (𝑗 + 𝑀) ∈ dom 𝑊)) → ((𝑊‘(𝑖 + 𝑀)) = (𝑊‘(𝑗 + 𝑀)) → (𝑖 + 𝑀) = (𝑗 + 𝑀)))
54	53	anassrs 467	. . . . . . . 8 ⊢ (((𝑊:dom 𝑊–1-1→𝐷 ∧ (𝑖 + 𝑀) ∈ dom 𝑊) ∧ (𝑗 + 𝑀) ∈ dom 𝑊) → ((𝑊‘(𝑖 + 𝑀)) = (𝑊‘(𝑗 + 𝑀)) → (𝑖 + 𝑀) = (𝑗 + 𝑀)))
55	54	imp 406	. . . . . . 7 ⊢ ((((𝑊:dom 𝑊–1-1→𝐷 ∧ (𝑖 + 𝑀) ∈ dom 𝑊) ∧ (𝑗 + 𝑀) ∈ dom 𝑊) ∧ (𝑊‘(𝑖 + 𝑀)) = (𝑊‘(𝑗 + 𝑀))) → (𝑖 + 𝑀) = (𝑗 + 𝑀))
56	22, 39, 43, 52, 55	syl1111anc 840	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → (𝑖 + 𝑀) = (𝑗 + 𝑀))
57	13, 17, 20, 56	addcan2ad 11326	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗)) → 𝑖 = 𝑗)
58	57	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)) → (((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) → 𝑖 = 𝑗))
59	58	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩) ∧ 𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩))) → (((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) → 𝑖 = 𝑗))
60	59	ralrimivva 3176	. 2 ⊢ (𝜑 → ∀𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)∀𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)(((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) → 𝑖 = 𝑗))
61		dff13 7194	. 2 ⊢ ((𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)–1-1→𝐷 ↔ ((𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)⟶𝐷 ∧ ∀𝑖 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)∀𝑗 ∈ dom (𝑊 substr ⟨𝑀, 𝑁⟩)(((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑖) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) → 𝑖 = 𝑗)))
62	6, 60, 61	sylanbrc 583	1 ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)–1-1→𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3048 ⊆ wss 3898 ⟨cop 4581 dom cdm 5619 ⟶wf 6482 –1-1→wf1 6483 ‘cfv 6486 (class class class)co 7352 0cc0 11013 + caddc 11016 − cmin 11351 ℤcz 12475 ℤ_≥cuz 12738 ...cfz 13409 ..^cfzo 13556 ♯chash 14239 Word cword 14422 substr csubstr 14550

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-card 9839 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-nn 12133 df-n0 12389 df-z 12476 df-uz 12739 df-fz 13410 df-fzo 13557 df-hash 14240 df-word 14423 df-substr 14551

This theorem is referenced by: cycpmco2f1 33100

W3C validator