Proof of Theorem elwwlks2
Step | Hyp | Ref
| Expression |
1 | | 2nn0 11186 |
. . 3
⊢ 2 ∈
ℕ0 |
2 | | elwwlks2.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
3 | 2 | wwlksnwwlksnon 41121 |
. . 3
⊢ ((2
∈ ℕ0 ∧ 𝐺 ∈ UPGraph ) → (𝑊 ∈ (2 WWalkSN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
4 | 1, 3 | mpan 702 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalkSN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
5 | 2 | elwwlks2on 41162 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)))) |
6 | 5 | 3expb 1258 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)))) |
7 | 6 | 2rexbidva 3038 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)))) |
8 | | rexcom 3080 |
. . . 4
⊢
(∃𝑐 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2))) |
9 | | s3cli 13476 |
. . . . . . . . . 10
⊢
〈“𝑎𝑏𝑐”〉 ∈ Word V |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → 〈“𝑎𝑏𝑐”〉 ∈ Word V) |
11 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑊 = 〈“𝑎𝑏𝑐”〉) |
12 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑝 = 〈“𝑎𝑏𝑐”〉) |
13 | 11, 12 | eqtr4d 2647 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑊 = 𝑝) |
14 | 13 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑓(1Walks‘𝐺)𝑊 ↔ 𝑓(1Walks‘𝐺)𝑝)) |
15 | 14 | biimpd 218 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑓(1Walks‘𝐺)𝑊 → 𝑓(1Walks‘𝐺)𝑝)) |
16 | 15 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑓(1Walks‘𝐺)𝑊 → (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑓(1Walks‘𝐺)𝑝)) |
17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2) → (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑓(1Walks‘𝐺)𝑝)) |
18 | 17 | impcom 445 |
. . . . . . . . . . 11
⊢
((((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → 𝑓(1Walks‘𝐺)𝑝) |
19 | | simprr 792 |
. . . . . . . . . . 11
⊢
((((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → (#‘𝑓) = 2) |
20 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑎 ∈ V |
21 | | s3fv0 13486 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ V →
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎) |
22 | 21 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ V → 𝑎 = (〈“𝑎𝑏𝑐”〉‘0)) |
23 | 20, 22 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑎 = (〈“𝑎𝑏𝑐”〉‘0)) |
24 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘0) = (〈“𝑎𝑏𝑐”〉‘0)) |
25 | 23, 24 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑎 = (𝑝‘0)) |
26 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑏 ∈ V |
27 | | s3fv1 13487 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ V →
(〈“𝑎𝑏𝑐”〉‘1) = 𝑏) |
28 | 27 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ V → 𝑏 = (〈“𝑎𝑏𝑐”〉‘1)) |
29 | 26, 28 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑏 = (〈“𝑎𝑏𝑐”〉‘1)) |
30 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘1) = (〈“𝑎𝑏𝑐”〉‘1)) |
31 | 29, 30 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑏 = (𝑝‘1)) |
32 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑐 ∈ V |
33 | | s3fv2 13488 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ V →
(〈“𝑎𝑏𝑐”〉‘2) = 𝑐) |
34 | 33 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ V → 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)) |
35 | 32, 34 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)) |
36 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘2) = (〈“𝑎𝑏𝑐”〉‘2)) |
37 | 35, 36 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑐 = (𝑝‘2)) |
38 | 25, 31, 37 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) |
39 | 38 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) |
40 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) |
41 | 18, 19, 40 | 3jca 1235 |
. . . . . . . . . 10
⊢
((((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) → (𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) |
42 | 41 | ex 449 |
. . . . . . . . 9
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2) → (𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
43 | 10, 42 | spcimedv 3265 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2) → ∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
44 | | 1wlklenvp1 40823 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓(1Walks‘𝐺)𝑝 → (#‘𝑝) = ((#‘𝑓) + 1)) |
45 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝑝) =
((#‘𝑓) + 1) ∧
(#‘𝑓) = 2) →
(#‘𝑝) =
((#‘𝑓) +
1)) |
46 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝑓) = 2
→ ((#‘𝑓) + 1) =
(2 + 1)) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝑝) =
((#‘𝑓) + 1) ∧
(#‘𝑓) = 2) →
((#‘𝑓) + 1) = (2 +
1)) |
48 | 45, 47 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝑝) =
((#‘𝑓) + 1) ∧
(#‘𝑓) = 2) →
(#‘𝑝) = (2 +
1)) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑝) = ((#‘𝑓) + 1) ∧ (#‘𝑓) = 2)) → (#‘𝑝) = (2 + 1)) |
50 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 + 1) =
3 |
51 | 49, 50 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑝) = ((#‘𝑓) + 1) ∧ (#‘𝑓) = 2)) → (#‘𝑝) = 3) |
52 | 51 | exp32 629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓(1Walks‘𝐺)𝑝 → ((#‘𝑝) = ((#‘𝑓) + 1) → ((#‘𝑓) = 2 → (#‘𝑝) = 3))) |
53 | 44, 52 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(1Walks‘𝐺)𝑝 → ((#‘𝑓) = 2 → (#‘𝑝) = 3)) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) → ((#‘𝑓) = 2 → (#‘𝑝) = 3)) |
55 | 54 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) → (#‘𝑝) = 3) |
56 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎) |
57 | 56 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝑝‘0) → (𝑝‘0) = 𝑎) |
58 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏) |
59 | 58 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑝‘1) → (𝑝‘1) = 𝑏) |
60 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐) |
61 | 60 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑝‘2) → (𝑝‘2) = 𝑐) |
62 | 57, 59, 61 | 3anim123i 1240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
63 | 55, 62 | anim12i 588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))) |
64 | 2 | 1wlkpwrd 40822 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(1Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
65 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
66 | 65 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
67 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
68 | 66, 67 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
70 | 64, 69 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) → (𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
71 | 70 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
72 | | eqwrds3 13552 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
74 | 63, 73 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 = 〈“𝑎𝑏𝑐”〉) |
75 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) → 𝑊 = 〈“𝑎𝑏𝑐”〉) |
76 | 75 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑊 = 〈“𝑎𝑏𝑐”〉) |
77 | 74, 76 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 = 𝑊) |
78 | 77 | breq2d 4595 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(1Walks‘𝐺)𝑝 ↔ 𝑓(1Walks‘𝐺)𝑊)) |
79 | 78 | biimpd 218 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(1Walks‘𝐺)𝑝 → 𝑓(1Walks‘𝐺)𝑊)) |
80 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (#‘𝑓) = 2) |
81 | 79, 80 | jctird 565 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓(1Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (#‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(1Walks‘𝐺)𝑝 → (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2))) |
82 | 81 | exp41 636 |
. . . . . . . . . . . . 13
⊢ (𝑓(1Walks‘𝐺)𝑝 → ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((#‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → (𝑓(1Walks‘𝐺)𝑝 → (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)))))) |
83 | 82 | com25 97 |
. . . . . . . . . . . 12
⊢ (𝑓(1Walks‘𝐺)𝑝 → (𝑓(1Walks‘𝐺)𝑝 → ((#‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)))))) |
84 | 83 | pm2.43i 50 |
. . . . . . . . . . 11
⊢ (𝑓(1Walks‘𝐺)𝑝 → ((#‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2))))) |
85 | 84 | 3imp 1249 |
. . . . . . . . . 10
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2))) |
86 | 85 | com12 32 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2))) |
87 | 86 | exlimdv 1848 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2))) |
88 | 43, 87 | impbid 201 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2) ↔ ∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
89 | 88 | exbidv 1837 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2) ↔ ∃𝑓∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
90 | 89 | pm5.32da 671 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) ↔ (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
91 | 90 | 2rexbidva 3038 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
92 | 8, 91 | syl5bb 271 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
93 | 92 | rexbidva 3031 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(1Walks‘𝐺)𝑊 ∧ (#‘𝑓) = 2)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
94 | 4, 7, 93 | 3bitrd 293 |
1
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalkSN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |