Proof of Theorem elwwlks2
| Step | Hyp | Ref
| Expression |
| 1 | | elwwlks2.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | 1 | wwlksnwwlksnon 29935 |
. . 3
⊢ (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
| 4 | 1 | elwwlks2on 29979 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))) |
| 5 | 4 | 3expb 1121 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))) |
| 6 | 5 | 2rexbidva 3220 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))) |
| 7 | | rexcom 3290 |
. . . 4
⊢
(∃𝑐 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))) |
| 8 | | s3cli 14920 |
. . . . . . . . . 10
⊢
〈“𝑎𝑏𝑐”〉 ∈ Word V |
| 9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → 〈“𝑎𝑏𝑐”〉 ∈ Word V) |
| 10 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑊 = 〈“𝑎𝑏𝑐”〉) |
| 11 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑝 = 〈“𝑎𝑏𝑐”〉) |
| 12 | 10, 11 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑊 = 𝑝) |
| 13 | 12 | breq2d 5155 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑓(Walks‘𝐺)𝑊 ↔ 𝑓(Walks‘𝐺)𝑝)) |
| 14 | 13 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑓(Walks‘𝐺)𝑊 → 𝑓(Walks‘𝐺)𝑝)) |
| 15 | 14 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑓(Walks‘𝐺)𝑊 → (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑓(Walks‘𝐺)𝑝)) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑓(Walks‘𝐺)𝑝)) |
| 17 | 16 | impcom 407 |
. . . . . . . . . . 11
⊢
((((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → 𝑓(Walks‘𝐺)𝑝) |
| 18 | | simprr 773 |
. . . . . . . . . . 11
⊢
((((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (♯‘𝑓) = 2) |
| 19 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑎 ∈ V |
| 20 | | s3fv0 14930 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ V →
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎) |
| 21 | 20 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ V → 𝑎 = (〈“𝑎𝑏𝑐”〉‘0)) |
| 22 | 19, 21 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑎 = (〈“𝑎𝑏𝑐”〉‘0)) |
| 23 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘0) = (〈“𝑎𝑏𝑐”〉‘0)) |
| 24 | 22, 23 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑎 = (𝑝‘0)) |
| 25 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑏 ∈ V |
| 26 | | s3fv1 14931 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ V →
(〈“𝑎𝑏𝑐”〉‘1) = 𝑏) |
| 27 | 26 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ V → 𝑏 = (〈“𝑎𝑏𝑐”〉‘1)) |
| 28 | 25, 27 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑏 = (〈“𝑎𝑏𝑐”〉‘1)) |
| 29 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘1) = (〈“𝑎𝑏𝑐”〉‘1)) |
| 30 | 28, 29 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑏 = (𝑝‘1)) |
| 31 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑐 ∈ V |
| 32 | | s3fv2 14932 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ V →
(〈“𝑎𝑏𝑐”〉‘2) = 𝑐) |
| 33 | 32 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ V → 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)) |
| 34 | 31, 33 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)) |
| 35 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘2) = (〈“𝑎𝑏𝑐”〉‘2)) |
| 36 | 34, 35 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑐 = (𝑝‘2)) |
| 37 | 24, 30, 36 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) |
| 40 | 17, 18, 39 | 3jca 1129 |
. . . . . . . . . 10
⊢
((((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) |
| 41 | 40 | ex 412 |
. . . . . . . . 9
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 42 | 9, 41 | spcimedv 3595 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → ∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 43 | | wlklenvp1 29636 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1)) |
| 44 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑝)
= ((♯‘𝑓) + 1)
∧ (♯‘𝑓) =
2) → (♯‘𝑝)
= ((♯‘𝑓) +
1)) |
| 45 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = (2 + 1)) |
| 46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑝)
= ((♯‘𝑓) + 1)
∧ (♯‘𝑓) =
2) → ((♯‘𝑓) + 1) = (2 + 1)) |
| 47 | 44, 46 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝑝)
= ((♯‘𝑓) + 1)
∧ (♯‘𝑓) =
2) → (♯‘𝑝)
= (2 + 1)) |
| 48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2)) →
(♯‘𝑝) = (2 +
1)) |
| 49 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 + 1) =
3 |
| 50 | 48, 49 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2)) →
(♯‘𝑝) =
3) |
| 51 | 50 | exp32 420 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑝) = ((♯‘𝑓) + 1) → ((♯‘𝑓) = 2 →
(♯‘𝑝) =
3))) |
| 52 | 43, 51 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3)) |
| 53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) → ((♯‘𝑓) = 2 →
(♯‘𝑝) =
3)) |
| 54 | 53 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) →
(♯‘𝑝) =
3) |
| 55 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎) |
| 56 | 55 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝑝‘0) → (𝑝‘0) = 𝑎) |
| 57 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏) |
| 58 | 57 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑝‘1) → (𝑝‘1) = 𝑏) |
| 59 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐) |
| 60 | 59 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑝‘2) → (𝑝‘2) = 𝑐) |
| 61 | 56, 58, 60 | 3anim123i 1152 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
| 62 | 54, 61 | anim12i 613 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))) |
| 63 | 1 | wlkpwrd 29635 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
| 64 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
| 65 | 64 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
| 66 | | 3anass 1095 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
| 67 | 65, 66 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
| 69 | 63, 68 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) → (𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
| 70 | 69 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
| 71 | | eqwrds3 15000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
| 72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
| 73 | 62, 72 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 = 〈“𝑎𝑏𝑐”〉) |
| 74 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) → 𝑊 = 〈“𝑎𝑏𝑐”〉) |
| 75 | 74 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑊 = 〈“𝑎𝑏𝑐”〉) |
| 76 | 73, 75 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 = 𝑊) |
| 77 | 76 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝 ↔ 𝑓(Walks‘𝐺)𝑊)) |
| 78 | 77 | biimpd 229 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑊)) |
| 79 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (♯‘𝑓) = 2) |
| 80 | 78, 79 | jctird 526 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝 → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))) |
| 81 | 80 | exp41 434 |
. . . . . . . . . . . . 13
⊢ (𝑓(Walks‘𝐺)𝑝 → ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((♯‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → (𝑓(Walks‘𝐺)𝑝 → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))))) |
| 82 | 81 | com25 99 |
. . . . . . . . . . . 12
⊢ (𝑓(Walks‘𝐺)𝑝 → (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))))) |
| 83 | 82 | pm2.43i 52 |
. . . . . . . . . . 11
⊢ (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))) |
| 84 | 83 | 3imp 1111 |
. . . . . . . . . 10
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))) |
| 85 | 84 | com12 32 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))) |
| 86 | 85 | exlimdv 1933 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))) |
| 87 | 42, 86 | impbid 212 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) ↔ ∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 88 | 87 | exbidv 1921 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) ↔ ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 89 | 88 | pm5.32da 579 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
| 90 | 89 | 2rexbidva 3220 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
| 91 | 7, 90 | bitrid 283 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
| 92 | 91 | rexbidva 3177 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
| 93 | 3, 6, 92 | 3bitrd 305 |
1
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |