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