Step | Hyp | Ref
| Expression |
1 | | numclwwlk.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | numclwwlk.q |
. . . . . 6
⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
3 | 1, 2 | numclwwlkovq 27232 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) |
4 | 3 | 3adant1 1079 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) |
5 | 4 | eleq2d 2687 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) ↔ 𝑊 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)})) |
6 | | fveq1 6190 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑤‘0) = (𝑊‘0)) |
7 | 6 | eqeq1d 2624 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((𝑤‘0) = 𝑋 ↔ (𝑊‘0) = 𝑋)) |
8 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ( lastS ‘𝑤) = ( lastS ‘𝑊)) |
9 | 8 | neeq1d 2853 |
. . . . 5
⊢ (𝑤 = 𝑊 → (( lastS ‘𝑤) ≠ 𝑋 ↔ ( lastS ‘𝑊) ≠ 𝑋)) |
10 | 7, 9 | anbi12d 747 |
. . . 4
⊢ (𝑤 = 𝑊 → (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) ↔ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) |
11 | 10 | elrab 3363 |
. . 3
⊢ (𝑊 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) |
12 | 5, 11 | syl6bb 276 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)))) |
13 | | simpl1 1064 |
. . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → 𝐺 ∈ FriendGraph ) |
14 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
15 | 1, 14 | wwlknp 26734 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
16 | | peano2nn 11032 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
17 | 16 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 + 1) ∈ ℕ) |
18 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) |
19 | 17, 18 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)))) |
20 | 19 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))))) |
21 | 20 | 3adant3 1081 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))))) |
22 | 15, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))))) |
23 | | lswlgt0cl 13356 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℕ ∧
(𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) → ( lastS ‘𝑊) ∈ 𝑉) |
24 | 22, 23 | syl6 35 |
. . . . . . . . . 10
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ → ( lastS ‘𝑊) ∈ 𝑉)) |
25 | 24 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → (𝑁 ∈ ℕ → ( lastS ‘𝑊) ∈ 𝑉)) |
26 | 25 | com12 32 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → ( lastS ‘𝑊) ∈ 𝑉)) |
27 | 26 | 3ad2ant3 1084 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → ( lastS ‘𝑊) ∈ 𝑉)) |
28 | 27 | imp 445 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → ( lastS ‘𝑊) ∈ 𝑉) |
29 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ ((𝑊‘0) = 𝑋 → ((𝑊‘0) ∈ 𝑉 ↔ 𝑋 ∈ 𝑉)) |
30 | 29 | biimprd 238 |
. . . . . . . . . 10
⊢ ((𝑊‘0) = 𝑋 → (𝑋 ∈ 𝑉 → (𝑊‘0) ∈ 𝑉)) |
31 | 30 | ad2antrl 764 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → (𝑋 ∈ 𝑉 → (𝑊‘0) ∈ 𝑉)) |
32 | 31 | com12 32 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → (𝑊‘0) ∈ 𝑉)) |
33 | 32 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → (𝑊‘0) ∈ 𝑉)) |
34 | 33 | imp 445 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → (𝑊‘0) ∈ 𝑉) |
35 | | neeq2 2857 |
. . . . . . . . . 10
⊢ (𝑋 = (𝑊‘0) → (( lastS ‘𝑊) ≠ 𝑋 ↔ ( lastS ‘𝑊) ≠ (𝑊‘0))) |
36 | 35 | eqcoms 2630 |
. . . . . . . . 9
⊢ ((𝑊‘0) = 𝑋 → (( lastS ‘𝑊) ≠ 𝑋 ↔ ( lastS ‘𝑊) ≠ (𝑊‘0))) |
37 | 36 | biimpa 501 |
. . . . . . . 8
⊢ (((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋) → ( lastS ‘𝑊) ≠ (𝑊‘0)) |
38 | 37 | adantl 482 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → ( lastS ‘𝑊) ≠ (𝑊‘0)) |
39 | 38 | adantl 482 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → ( lastS ‘𝑊) ≠ (𝑊‘0)) |
40 | 28, 34, 39 | 3jca 1242 |
. . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → (( lastS ‘𝑊) ∈ 𝑉 ∧ (𝑊‘0) ∈ 𝑉 ∧ ( lastS ‘𝑊) ≠ (𝑊‘0))) |
41 | 1, 14 | frcond2 27131 |
. . . . 5
⊢ (𝐺 ∈ FriendGraph → (((
lastS ‘𝑊) ∈
𝑉 ∧ (𝑊‘0) ∈ 𝑉 ∧ ( lastS ‘𝑊) ≠ (𝑊‘0)) → ∃!𝑣 ∈ 𝑉 ({( lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)))) |
42 | 13, 40, 41 | sylc 65 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → ∃!𝑣 ∈ 𝑉 ({( lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) |
43 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → 𝑊 ∈ (𝑁 WWalksN 𝐺)) |
44 | 43 | ad2antlr 763 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑊 ∈ (𝑁 WWalksN 𝐺)) |
45 | | simpr 477 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
46 | | nnnn0 11299 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
47 | 46 | 3ad2ant3 1084 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) |
48 | 47 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑁 ∈
ℕ0) |
49 | 44, 45, 48 | 3jca 1242 |
. . . . . . . 8
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
50 | 1, 14 | wwlksext2clwwlk 26924 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({(
lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) |
51 | 50 | imp 445 |
. . . . . . . 8
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ ({( lastS
‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) |
52 | 49, 51 | sylan 488 |
. . . . . . 7
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ ({( lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) |
53 | 1 | wwlknbp 26733 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) |
54 | 53 | simp3d 1075 |
. . . . . . . . . 10
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑊 ∈ Word 𝑉) |
55 | 54 | ad2antrl 764 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → 𝑊 ∈ Word 𝑉) |
56 | 55 | ad2antrr 762 |
. . . . . . . 8
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → 𝑊 ∈ Word 𝑉) |
57 | 45 | adantr 481 |
. . . . . . . 8
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → 𝑣 ∈ 𝑉) |
58 | | 2z 11409 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
59 | | nn0pzuz 11745 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 2 ∈ ℤ) → (𝑁 + 2) ∈
(ℤ≥‘2)) |
60 | 46, 58, 59 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
(ℤ≥‘2)) |
61 | 60 | 3ad2ant3 1084 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑁 + 2) ∈
(ℤ≥‘2)) |
62 | 61 | ad3antrrr 766 |
. . . . . . . 8
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → (𝑁 + 2) ∈
(ℤ≥‘2)) |
63 | | simpr 477 |
. . . . . . . 8
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) |
64 | 1, 14 | clwwlksext2edg 26923 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑣 ∈ 𝑉 ∧ (𝑁 + 2) ∈
(ℤ≥‘2)) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → ({( lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) |
65 | 56, 57, 62, 63, 64 | syl31anc 1329 |
. . . . . . 7
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → ({( lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) |
66 | 52, 65 | impbida 877 |
. . . . . 6
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (({( lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) |
67 | 47 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → 𝑁 ∈
ℕ0) |
68 | 1 | eleq2i 2693 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ (Vtx‘𝐺)) |
69 | 68 | biimpi 206 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑉 → 𝑣 ∈ (Vtx‘𝐺)) |
70 | 67, 69 | anim12i 590 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑁 ∈ ℕ0 ∧ 𝑣 ∈ (Vtx‘𝐺))) |
71 | 37 | anim2i 593 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑊) ≠ (𝑊‘0))) |
72 | 71 | ad2antlr 763 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑊) ≠ (𝑊‘0))) |
73 | | clwwlkextfrlem1 27208 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑣 ∈
(Vtx‘𝐺)) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑊) ≠ (𝑊‘0))) → (((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ (𝑊‘0))) |
74 | 70, 72, 73 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ (𝑊‘0))) |
75 | | eqeq2 2633 |
. . . . . . . . . . . . 13
⊢ (𝑋 = (𝑊‘0) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0))) |
76 | 75 | eqcoms 2630 |
. . . . . . . . . . . 12
⊢ ((𝑊‘0) = 𝑋 → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0))) |
77 | 76 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0))) |
78 | 77 | ad2antlr 763 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0))) |
79 | 74 | simpld 475 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0)) |
80 | 79 | neeq2d 2854 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0) ↔ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ (𝑊‘0))) |
81 | 78, 80 | anbi12d 747 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)) ↔ (((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ (𝑊‘0)))) |
82 | 74, 81 | mpbird 247 |
. . . . . . . 8
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) |
83 | | nncn 11028 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
84 | | 2cnd 11093 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
85 | 83, 84 | pncand 10393 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑁 + 2) − 2) = 𝑁) |
86 | 85 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑁 + 2) − 2) = 𝑁) |
87 | 86 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑁 + 2) − 2) = 𝑁) |
88 | 87 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) = ((𝑊 ++ 〈“𝑣”〉)‘𝑁)) |
89 | 88 | neeq1d 2853 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0) ↔ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) |
90 | 89 | anbi2d 740 |
. . . . . . . 8
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)) ↔ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)))) |
91 | 82, 90 | mpbird 247 |
. . . . . . 7
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) |
92 | 91 | biantrud 528 |
. . . . . 6
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ ((𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))))) |
93 | | 2nn 11185 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
94 | | nnaddcl 11042 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 2 ∈
ℕ) → (𝑁 + 2)
∈ ℕ) |
95 | 93, 94 | mpan2 707 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
ℕ) |
96 | 95 | anim2i 593 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ ℕ)) |
97 | 96 | 3adant1 1079 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ ℕ)) |
98 | 97 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ ℕ)) |
99 | | numclwwlk.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
100 | | numclwwlk.h |
. . . . . . . . . 10
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))}) |
101 | 1, 2, 99, 100 | numclwwlkovh 27234 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ ℕ) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) |
102 | 98, 101 | syl 17 |
. . . . . . . 8
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) |
103 | 102 | eleq2d 2687 |
. . . . . . 7
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑊 ++ 〈“𝑣”〉) ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})) |
104 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → (𝑤‘0) = ((𝑊 ++ 〈“𝑣”〉)‘0)) |
105 | 104 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → ((𝑤‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋)) |
106 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → (𝑤‘((𝑁 + 2) − 2)) = ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2))) |
107 | 106, 104 | neeq12d 2855 |
. . . . . . . . 9
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → ((𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0) ↔ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) |
108 | 105, 107 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0)) ↔ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)))) |
109 | 108 | elrab 3363 |
. . . . . . 7
⊢ ((𝑊 ++ 〈“𝑣”〉) ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ ((𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)))) |
110 | 103, 109 | syl6rbb 277 |
. . . . . 6
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) ↔ (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
111 | 66, 92, 110 | 3bitrd 294 |
. . . . 5
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (({( lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
112 | 111 | reubidva 3125 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → (∃!𝑣 ∈ 𝑉 ({( lastS ‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ ∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
113 | 42, 112 | mpbid 222 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋))) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) |
114 | 113 | ex 450 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ ( lastS ‘𝑊) ≠ 𝑋)) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
115 | 12, 114 | sylbid 230 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |