Step | Hyp | Ref
| Expression |
1 | | clwwlkbij.d |
. . 3
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} |
2 | | clwwlkbij.f |
. . 3
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) |
3 | 1, 2 | clwwlkf 26322 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷⟶((𝑉 ClWWalksN 𝐸)‘𝑁)) |
4 | 1, 2 | clwwlkfv 26323 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (𝑥 substr 〈0, 𝑁〉)) |
5 | 1, 2 | clwwlkfv 26323 |
. . . . . 6
⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) = (𝑦 substr 〈0, 𝑁〉)) |
6 | 4, 5 | eqeqan12d 2626 |
. . . . 5
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉))) |
7 | 6 | adantl 481 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉))) |
8 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → ( lastS ‘𝑤) = ( lastS ‘𝑥)) |
9 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0)) |
10 | 8, 9 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘𝑥) = (𝑥‘0))) |
11 | 10, 1 | elrab2 3333 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑥) = (𝑥‘0))) |
12 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ( lastS ‘𝑤) = ( lastS ‘𝑦)) |
13 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
14 | 12, 13 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘𝑦) = (𝑦‘0))) |
15 | 14, 1 | elrab2 3333 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐷 ↔ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑦) = (𝑦‘0))) |
16 | 11, 15 | anbi12i 729 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ↔ ((𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑦) = (𝑦‘0)))) |
17 | | wwlknimp 26215 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥‘𝑖), (𝑥‘(𝑖 + 1))} ∈ ran 𝐸)) |
18 | | wwlknimp 26215 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ ran 𝐸)) |
19 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (#‘𝑥) = (𝑁 + 1)) |
20 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (#‘𝑦) = (𝑁 + 1)) |
21 | 19, 20 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (#‘𝑥) = (#‘𝑦)) |
22 | 21 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → (#‘𝑥) = (#‘𝑦)) |
23 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
24 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 1 ∈
ℂ |
25 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
26 | 25 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → 𝑁 = ((𝑁 + 1) −
1)) |
27 | 23, 24, 26 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 + 1) − 1)) |
28 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝑥) =
(𝑁 + 1) →
((#‘𝑥) − 1) =
((𝑁 + 1) −
1)) |
29 | 28 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝑥) =
(𝑁 + 1) → ((𝑁 + 1) − 1) =
((#‘𝑥) −
1)) |
30 | 27, 29 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝑥) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) → 𝑁 = ((#‘𝑥) − 1)) |
31 | 30 | opeq2d 4347 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝑥) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) → 〈0,
𝑁〉 = 〈0,
((#‘𝑥) −
1)〉) |
32 | 31 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝑥) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑥 substr 〈0, 𝑁〉) = (𝑥 substr 〈0, ((#‘𝑥) − 1)〉)) |
33 | 31 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝑥) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) → (𝑦 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉)) |
34 | 32, 33 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝑥) =
(𝑁 + 1) ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉))) |
35 | 34 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑥) =
(𝑁 + 1) → (𝑁 ∈ ℕ → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉)))) |
36 | 35 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉)))) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉)))) |
38 | 37 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉))) |
39 | 38 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → (𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉)) |
40 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) → 𝑦 ∈ Word 𝑉) |
41 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → 𝑥 ∈ Word 𝑉) |
42 | 40, 41 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉)) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉)) |
44 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
45 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ∈
ℕ0 |
46 | 44, 45 | jctil 558 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → (0 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) |
48 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
49 | 48 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁 + 1)) |
50 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝑥) =
(𝑁 + 1) → (𝑁 ≤ (#‘𝑥) ↔ 𝑁 ≤ (𝑁 + 1))) |
51 | 49, 50 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑥) =
(𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (#‘𝑥))) |
52 | 51 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (#‘𝑥))) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (#‘𝑥))) |
54 | 53 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (#‘𝑥)) |
55 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝑦) =
(𝑁 + 1) → (𝑁 ≤ (#‘𝑦) ↔ 𝑁 ≤ (𝑁 + 1))) |
56 | 49, 55 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑦) =
(𝑁 + 1) → (𝑁 ∈ ℕ → 𝑁 ≤ (#‘𝑦))) |
57 | 56 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) → (𝑁 ∈ ℕ → 𝑁 ≤ (#‘𝑦))) |
58 | 57 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 𝑁 ≤ (#‘𝑦))) |
59 | 58 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → 𝑁 ≤ (#‘𝑦)) |
60 | | swrdspsleq 13301 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉) ∧ (0 ∈ ℕ0 ∧
𝑁 ∈
ℕ0) ∧ (𝑁 ≤ (#‘𝑥) ∧ 𝑁 ≤ (#‘𝑦))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))) |
61 | 43, 47, 54, 59, 60 | syl112anc 1322 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) ↔ ∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))) |
62 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
63 | 62 | biimpri 217 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 0 ∈
(0..^𝑁)) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → 0 ∈ (0..^𝑁)) |
65 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = 0 → (𝑥‘𝑖) = (𝑥‘0)) |
66 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = 0 → (𝑦‘𝑖) = (𝑦‘0)) |
67 | 65, 66 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = 0 → ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑥‘0) = (𝑦‘0))) |
68 | 67 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ∈
(0..^𝑁) →
(∀𝑖 ∈
(0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖) → (𝑥‘0) = (𝑦‘0))) |
69 | 64, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → (∀𝑖 ∈ (0..^𝑁)(𝑥‘𝑖) = (𝑦‘𝑖) → (𝑥‘0) = (𝑦‘0))) |
70 | 61, 69 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → (𝑥‘0) = (𝑦‘0))) |
71 | 70 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → (𝑥‘0) = (𝑦‘0)) |
72 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → ( lastS ‘𝑥) = (𝑥‘0)) |
73 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) → ( lastS ‘𝑦) = (𝑦‘0)) |
74 | 72, 73 | eqeqan12rd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (( lastS ‘𝑥) = ( lastS ‘𝑦) ↔ (𝑥‘0) = (𝑦‘0))) |
75 | 74 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → (( lastS ‘𝑥) = ( lastS ‘𝑦) ↔ (𝑥‘0) = (𝑦‘0))) |
76 | 71, 75 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → ( lastS ‘𝑥) = ( lastS ‘𝑦)) |
77 | 22, 39, 76 | jca32 556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → ((#‘𝑥) = (#‘𝑦) ∧ ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉) ∧ ( lastS
‘𝑥) = ( lastS
‘𝑦)))) |
78 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → 𝑥 ∈ Word 𝑉) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → 𝑥 ∈ Word 𝑉) |
80 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → 𝑦 ∈ Word 𝑉) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → 𝑦 ∈ Word 𝑉) |
82 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
83 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
84 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 <
1 |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 0 <
1) |
86 | 48, 82, 83, 85 | addgt0d 10481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 0 <
(𝑁 + 1)) |
87 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑥) =
(𝑁 + 1) → (0 <
(#‘𝑥) ↔ 0 <
(𝑁 + 1))) |
88 | 86, 87 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑥) =
(𝑁 + 1) → (𝑁 ∈ ℕ → 0 <
(#‘𝑥))) |
89 | 88 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → (𝑁 ∈ ℕ → 0 < (#‘𝑥))) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → (𝑁 ∈ ℕ → 0 < (#‘𝑥))) |
91 | 90 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → 0 < (#‘𝑥)) |
92 | 79, 81, 91 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) → (𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉 ∧ 0 < (#‘𝑥))) |
93 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → (𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉 ∧ 0 < (#‘𝑥))) |
94 | | 2swrd1eqwrdeq 13306 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉 ∧ 0 < (#‘𝑥)) → (𝑥 = 𝑦 ↔ ((#‘𝑥) = (#‘𝑦) ∧ ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉) ∧ ( lastS
‘𝑥) = ( lastS
‘𝑦))))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → (𝑥 = 𝑦 ↔ ((#‘𝑥) = (#‘𝑦) ∧ ((𝑥 substr 〈0, ((#‘𝑥) − 1)〉) = (𝑦 substr 〈0, ((#‘𝑥) − 1)〉) ∧ ( lastS
‘𝑥) = ( lastS
‘𝑦))))) |
96 | 77, 95 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)))) ∧ (𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉)) → 𝑥 = 𝑦) |
97 | 96 | exp31 628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))) |
98 | 97 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) ∧ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))) |
99 | 98 | expdcom 454 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ ( lastS ‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦)))) |
100 | 99 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) → (( lastS ‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))))) |
101 | 100 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ ran 𝐸) → (( lastS ‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))))) |
102 | 18, 101 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (( lastS ‘𝑦) = (𝑦‘0) → (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))))) |
103 | 102 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑦) = (𝑦‘0)) → (((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) ∧ ( lastS ‘𝑥) = (𝑥‘0)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦)))) |
104 | 103 | expdcom 454 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1)) → (( lastS ‘𝑥) = (𝑥‘0) → ((𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑦) = (𝑦‘0)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))))) |
105 | 104 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑥‘𝑖), (𝑥‘(𝑖 + 1))} ∈ ran 𝐸) → (( lastS ‘𝑥) = (𝑥‘0) → ((𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑦) = (𝑦‘0)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))))) |
106 | 17, 105 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (( lastS ‘𝑥) = (𝑥‘0) → ((𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑦) = (𝑦‘0)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))))) |
107 | 106 | imp31 447 |
. . . . . . 7
⊢ (((𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑦) = (𝑦‘0))) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))) |
108 | 107 | com12 32 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (((𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑥) = (𝑥‘0)) ∧ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑦) = (𝑦‘0))) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))) |
109 | 16, 108 | syl5bi 231 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦))) |
110 | 109 | imp 444 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝑥 substr 〈0, 𝑁〉) = (𝑦 substr 〈0, 𝑁〉) → 𝑥 = 𝑦)) |
111 | 7, 110 | sylbid 229 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
112 | 111 | ralrimivva 2954 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
113 | | dff13 6416 |
. 2
⊢ (𝐹:𝐷–1-1→((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝐹:𝐷⟶((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
114 | 3, 112, 113 | sylanbrc 695 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷–1-1→((𝑉 ClWWalksN 𝐸)‘𝑁)) |