Step | Hyp | Ref
| Expression |
1 | | clwwlknimp 26304 |
. . . 4
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸)) |
2 | | simplr2 1097 |
. . . . . 6
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → 𝑋 ∈ 𝑉) |
3 | | simplr1 1096 |
. . . . . . 7
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → 𝑉 USGrph 𝐸) |
4 | | eluzelcn 11575 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
5 | | 1e2m1 11013 |
. . . . . . . . . . . . . . . . 17
⊢ 1 = (2
− 1) |
6 | 5 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → 1 = (2
− 1)) |
7 | 6 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → (𝑁 − 1) = (𝑁 − (2 − 1))) |
8 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → 𝑁 ∈
ℂ) |
9 | | 2cnd 10970 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → 2 ∈
ℂ) |
10 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℂ → 1 ∈
ℂ) |
11 | 8, 9, 10 | subsubd 10299 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → (𝑁 − (2 − 1)) =
((𝑁 − 2) +
1)) |
12 | 7, 11 | eqtr2d 2645 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℂ → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
13 | 4, 12 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
14 | 13 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑤‘((𝑁 − 2) + 1)) = (𝑤‘(𝑁 − 1))) |
15 | 14 | preq2d 4219 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → {(𝑤‘(𝑁 − 2)), (𝑤‘((𝑁 − 2) + 1))} = {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))}) |
16 | 15 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ {(𝑤‘(𝑁 − 2)), (𝑤‘((𝑁 − 2) + 1))} = {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))}) |
17 | 16 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {(𝑤‘(𝑁 − 2)), (𝑤‘((𝑁 − 2) + 1))} = {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))}) |
18 | | ige2m2fzo 12398 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
19 | 18 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 2) ∈
(0..^(𝑁 −
1))) |
20 | | simp2 1055 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) |
21 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑁 − 2) → (𝑤‘𝑖) = (𝑤‘(𝑁 − 2))) |
22 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑁 − 2) → (𝑖 + 1) = ((𝑁 − 2) + 1)) |
23 | 22 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑁 − 2) → (𝑤‘(𝑖 + 1)) = (𝑤‘((𝑁 − 2) + 1))) |
24 | 21, 23 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑁 − 2) → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘(𝑁 − 2)), (𝑤‘((𝑁 − 2) + 1))}) |
25 | 24 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑁 − 2) → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑤‘(𝑁 − 2)), (𝑤‘((𝑁 − 2) + 1))} ∈ ran 𝐸)) |
26 | 25 | rspcva 3280 |
. . . . . . . . . 10
⊢ (((𝑁 − 2) ∈ (0..^(𝑁 − 1)) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) → {(𝑤‘(𝑁 − 2)), (𝑤‘((𝑁 − 2) + 1))} ∈ ran 𝐸) |
27 | 19, 20, 26 | syl2anr 494 |
. . . . . . . . 9
⊢ ((((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {(𝑤‘(𝑁 − 2)), (𝑤‘((𝑁 − 2) + 1))} ∈ ran 𝐸) |
28 | 17, 27 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))} ∈ ran 𝐸) |
29 | 28 | adantr 480 |
. . . . . . 7
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))} ∈ ran 𝐸) |
30 | | usgraedgrnv 25906 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))} ∈ ran 𝐸) → ((𝑤‘(𝑁 − 2)) ∈ 𝑉 ∧ (𝑤‘(𝑁 − 1)) ∈ 𝑉)) |
31 | 30 | simprd 478 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))} ∈ ran 𝐸) → (𝑤‘(𝑁 − 1)) ∈ 𝑉) |
32 | 3, 29, 31 | syl2anc 691 |
. . . . . 6
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ 𝑉) |
33 | | preq1 4212 |
. . . . . . . . . . 11
⊢ (𝑋 = (𝑤‘0) → {𝑋, (𝑤‘(𝑁 − 1))} = {(𝑤‘0), (𝑤‘(𝑁 − 1))}) |
34 | 33 | eqcoms 2618 |
. . . . . . . . . 10
⊢ ((𝑤‘0) = 𝑋 → {𝑋, (𝑤‘(𝑁 − 1))} = {(𝑤‘0), (𝑤‘(𝑁 − 1))}) |
35 | | preq1 4212 |
. . . . . . . . . . 11
⊢ ((𝑤‘0) = (𝑤‘(𝑁 − 2)) → {(𝑤‘0), (𝑤‘(𝑁 − 1))} = {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))}) |
36 | 35 | eqcoms 2618 |
. . . . . . . . . 10
⊢ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → {(𝑤‘0), (𝑤‘(𝑁 − 1))} = {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))}) |
37 | 34, 36 | sylan9eq 2664 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {𝑋, (𝑤‘(𝑁 − 1))} = {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))}) |
38 | 37 | eleq1d 2672 |
. . . . . . . 8
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ({𝑋, (𝑤‘(𝑁 − 1))} ∈ ran 𝐸 ↔ {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))} ∈ ran 𝐸)) |
39 | 38 | adantl 481 |
. . . . . . 7
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ({𝑋, (𝑤‘(𝑁 − 1))} ∈ ran 𝐸 ↔ {(𝑤‘(𝑁 − 2)), (𝑤‘(𝑁 − 1))} ∈ ran 𝐸)) |
40 | 29, 39 | mpbird 246 |
. . . . . 6
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {𝑋, (𝑤‘(𝑁 − 1))} ∈ ran 𝐸) |
41 | | usgrav 25867 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
42 | 41 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑉 ∈ V ∧
𝐸 ∈
V)) |
43 | 42 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ (𝑉 ∈ V ∧
𝐸 ∈
V)) |
44 | 43 | adantr 480 |
. . . . . . 7
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
45 | | nbgrael 25955 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ↔ (𝑋 ∈ 𝑉 ∧ (𝑤‘(𝑁 − 1)) ∈ 𝑉 ∧ {𝑋, (𝑤‘(𝑁 − 1))} ∈ ran 𝐸))) |
46 | 44, 45 | syl 17 |
. . . . . 6
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ↔ (𝑋 ∈ 𝑉 ∧ (𝑤‘(𝑁 − 1)) ∈ 𝑉 ∧ {𝑋, (𝑤‘(𝑁 − 1))} ∈ ran 𝐸))) |
47 | 2, 32, 40, 46 | mpbir3and 1238 |
. . . . 5
⊢
(((((𝑤 ∈ Word
𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) |
48 | 47 | exp31 628 |
. . . 4
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (((𝑤‘0) =
𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)))) |
49 | 1, 48 | syl 17 |
. . 3
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (((𝑤‘0) =
𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)))) |
50 | 49 | impcom 445 |
. 2
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) |
51 | 50 | imp 444 |
1
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘(𝑁 − 1)) ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) |