| Step | Hyp | Ref
| Expression |
| 1 | | numclwwlk.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | numclwwlk.q |
. . . . . 6
⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)}) |
| 3 | 1, 2 | numclwwlkovq 30393 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}) |
| 4 | 3 | 3adant1 1131 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}) |
| 5 | 4 | eleq2d 2827 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) ↔ 𝑊 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)})) |
| 6 | | fveq1 6905 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑤‘0) = (𝑊‘0)) |
| 7 | 6 | eqeq1d 2739 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((𝑤‘0) = 𝑋 ↔ (𝑊‘0) = 𝑋)) |
| 8 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (lastS‘𝑤) = (lastS‘𝑊)) |
| 9 | 8 | neeq1d 3000 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((lastS‘𝑤) ≠ 𝑋 ↔ (lastS‘𝑊) ≠ 𝑋)) |
| 10 | 7, 9 | anbi12d 632 |
. . . 4
⊢ (𝑤 = 𝑊 → (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) ↔ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) |
| 11 | 10 | elrab 3692 |
. . 3
⊢ (𝑊 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)} ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) |
| 12 | 5, 11 | bitrdi 287 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)))) |
| 13 | | simpl1 1192 |
. . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → 𝐺 ∈ FriendGraph ) |
| 14 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 15 | 1, 14 | wwlknp 29863 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 16 | | peano2nn 12278 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 + 1) ∈ ℕ) |
| 18 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1))) |
| 19 | 17, 18 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)))) |
| 20 | 19 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1))))) |
| 21 | 20 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1))))) |
| 22 | 15, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1))))) |
| 23 | | lswlgt0cl 14607 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℕ ∧
(𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1))) → (lastS‘𝑊) ∈ 𝑉) |
| 24 | 22, 23 | syl6 35 |
. . . . . . . . . 10
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ → (lastS‘𝑊) ∈ 𝑉)) |
| 25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑁 ∈ ℕ → (lastS‘𝑊) ∈ 𝑉)) |
| 26 | 25 | com12 32 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (lastS‘𝑊) ∈ 𝑉)) |
| 27 | 26 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (lastS‘𝑊) ∈ 𝑉)) |
| 28 | 27 | imp 406 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → (lastS‘𝑊) ∈ 𝑉) |
| 29 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ ((𝑊‘0) = 𝑋 → ((𝑊‘0) ∈ 𝑉 ↔ 𝑋 ∈ 𝑉)) |
| 30 | 29 | biimprd 248 |
. . . . . . . . . 10
⊢ ((𝑊‘0) = 𝑋 → (𝑋 ∈ 𝑉 → (𝑊‘0) ∈ 𝑉)) |
| 31 | 30 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑋 ∈ 𝑉 → (𝑊‘0) ∈ 𝑉)) |
| 32 | 31 | com12 32 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑊‘0) ∈ 𝑉)) |
| 33 | 32 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑊‘0) ∈ 𝑉)) |
| 34 | 33 | imp 406 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → (𝑊‘0) ∈ 𝑉) |
| 35 | | neeq2 3004 |
. . . . . . . . . 10
⊢ (𝑋 = (𝑊‘0) → ((lastS‘𝑊) ≠ 𝑋 ↔ (lastS‘𝑊) ≠ (𝑊‘0))) |
| 36 | 35 | eqcoms 2745 |
. . . . . . . . 9
⊢ ((𝑊‘0) = 𝑋 → ((lastS‘𝑊) ≠ 𝑋 ↔ (lastS‘𝑊) ≠ (𝑊‘0))) |
| 37 | 36 | biimpa 476 |
. . . . . . . 8
⊢ (((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋) → (lastS‘𝑊) ≠ (𝑊‘0)) |
| 38 | 37 | adantl 481 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (lastS‘𝑊) ≠ (𝑊‘0)) |
| 39 | 38 | adantl 481 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → (lastS‘𝑊) ≠ (𝑊‘0)) |
| 40 | 28, 34, 39 | 3jca 1129 |
. . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → ((lastS‘𝑊) ∈ 𝑉 ∧ (𝑊‘0) ∈ 𝑉 ∧ (lastS‘𝑊) ≠ (𝑊‘0))) |
| 41 | 1, 14 | frcond2 30286 |
. . . . 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 482 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → 𝑊 ∈ (𝑁 WWalksN 𝐺)) |
| 44 | 43 | ad2antlr 727 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑊 ∈ (𝑁 WWalksN 𝐺)) |
| 45 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
| 46 | | nnnn0 12533 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 47 | 46 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) |
| 48 | 47 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑁 ∈
ℕ0) |
| 49 | 44, 45, 48 | 3jca 1129 |
. . . . . . . 8
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
| 50 | 1, 14 | wwlksext2clwwlk 30076 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉) → (({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) |
| 51 | 50 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) |
| 52 | 51 | imp 406 |
. . . . . . . 8
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) |
| 53 | 49, 52 | sylan 580 |
. . . . . . 7
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) |
| 54 | 1 | wwlknbp 29862 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) |
| 55 | 54 | simp3d 1145 |
. . . . . . . . . 10
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑊 ∈ Word 𝑉) |
| 56 | 55 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → 𝑊 ∈ Word 𝑉) |
| 57 | 56 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → 𝑊 ∈ Word 𝑉) |
| 58 | 45 | adantr 480 |
. . . . . . . 8
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → 𝑣 ∈ 𝑉) |
| 59 | | 2z 12649 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
| 60 | | nn0pzuz 12947 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 2 ∈ ℤ) → (𝑁 + 2) ∈
(ℤ≥‘2)) |
| 61 | 46, 59, 60 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
(ℤ≥‘2)) |
| 62 | 61 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑁 + 2) ∈
(ℤ≥‘2)) |
| 63 | 62 | ad3antrrr 730 |
. . . . . . . 8
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → (𝑁 + 2) ∈
(ℤ≥‘2)) |
| 64 | | simpr 484 |
. . . . . . . 8
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) |
| 65 | 1, 14 | clwwlkext2edg 30075 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑣 ∈ 𝑉 ∧ (𝑁 + 2) ∈
(ℤ≥‘2)) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) |
| 66 | 57, 58, 63, 64, 65 | syl31anc 1375 |
. . . . . . 7
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑋 ∈
𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) |
| 67 | 53, 66 | impbida 801 |
. . . . . 6
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) |
| 68 | 45, 1 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (Vtx‘𝐺)) |
| 69 | 37 | anim2i 617 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑊) ≠ (𝑊‘0))) |
| 70 | 69 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑊) ≠ (𝑊‘0))) |
| 71 | 70 | simprd 495 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (lastS‘𝑊) ≠ (𝑊‘0)) |
| 72 | | numclwwlk2lem1lem 30361 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑊) ≠ (𝑊‘0)) → (((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ (𝑊‘0))) |
| 73 | 68, 44, 71, 72 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ (𝑊‘0))) |
| 74 | | eqeq2 2749 |
. . . . . . . . . . . . 13
⊢ (𝑋 = (𝑊‘0) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0))) |
| 75 | 74 | eqcoms 2745 |
. . . . . . . . . . . 12
⊢ ((𝑊‘0) = 𝑋 → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0))) |
| 76 | 75 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0))) |
| 77 | 76 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0))) |
| 78 | 73 | simpld 494 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0)) |
| 79 | 78 | neeq2d 3001 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0) ↔ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ (𝑊‘0))) |
| 80 | 77, 79 | anbi12d 632 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)) ↔ (((𝑊 ++ 〈“𝑣”〉)‘0) = (𝑊‘0) ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ (𝑊‘0)))) |
| 81 | 73, 80 | mpbird 257 |
. . . . . . . 8
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) |
| 82 | | nncn 12274 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 83 | | 2cnd 12344 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
| 84 | 82, 83 | pncand 11621 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑁 + 2) − 2) = 𝑁) |
| 85 | 84 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑁 + 2) − 2) = 𝑁) |
| 86 | 85 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑁 + 2) − 2) = 𝑁) |
| 87 | 86 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) = ((𝑊 ++ 〈“𝑣”〉)‘𝑁)) |
| 88 | 87 | neeq1d 3000 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0) ↔ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) |
| 89 | 88 | anbi2d 630 |
. . . . . . . 8
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)) ↔ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘𝑁) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)))) |
| 90 | 81, 89 | mpbird 257 |
. . . . . . 7
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) |
| 91 | 90 | biantrud 531 |
. . . . . 6
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ ((𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))))) |
| 92 | 61 | anim2i 617 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈
(ℤ≥‘2))) |
| 93 | 92 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈
(ℤ≥‘2))) |
| 94 | 93 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈
(ℤ≥‘2))) |
| 95 | | numclwwlk.h |
. . . . . . . . . 10
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣}) |
| 96 | 95 | numclwwlkovh 30392 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈
(ℤ≥‘2)) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) |
| 97 | 94, 96 | syl 17 |
. . . . . . . 8
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}) |
| 98 | 97 | eleq2d 2827 |
. . . . . . 7
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑊 ++ 〈“𝑣”〉) ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})) |
| 99 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → (𝑤‘0) = ((𝑊 ++ 〈“𝑣”〉)‘0)) |
| 100 | 99 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → ((𝑤‘0) = 𝑋 ↔ ((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋)) |
| 101 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → (𝑤‘((𝑁 + 2) − 2)) = ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2))) |
| 102 | 101, 99 | neeq12d 3002 |
. . . . . . . . 9
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → ((𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0) ↔ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) |
| 103 | 100, 102 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑤 = (𝑊 ++ 〈“𝑣”〉) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0)) ↔ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)))) |
| 104 | 103 | elrab 3692 |
. . . . . . 7
⊢ ((𝑊 ++ 〈“𝑣”〉) ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ ((𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0)))) |
| 105 | 98, 104 | bitr2di 288 |
. . . . . 6
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ 〈“𝑣”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑣”〉)‘0) = 𝑋 ∧ ((𝑊 ++ 〈“𝑣”〉)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ 〈“𝑣”〉)‘0))) ↔ (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
| 106 | 67, 91, 105 | 3bitrd 305 |
. . . . 5
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
| 107 | 106 | reubidva 3396 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → (∃!𝑣 ∈ 𝑉 ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ ∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
| 108 | 42, 107 | mpbid 232 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2))) |
| 109 | 108 | ex 412 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |
| 110 | 12, 109 | sylbid 240 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ (𝑋𝐻(𝑁 + 2)))) |