Proof of Theorem elwspths2spth
| Step | Hyp | Ref
| Expression |
| 1 | | elwwlks2.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | 1 | wspthsnwspthsnon 29936 |
. . 3
⊢ (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))) |
| 4 | 1 | elwspths2on 29980 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
| 5 | 4 | 3expb 1121 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
| 6 | 5 | 2rexbidva 3220 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
| 7 | | rexcom 3290 |
. . . 4
⊢
(∃𝑐 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))) |
| 8 | | wspthnon 29878 |
. . . . . . 7
⊢
(〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉)) |
| 9 | | ancom 460 |
. . . . . . . . 9
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
| 10 | | 19.41v 1949 |
. . . . . . . . 9
⊢
(∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
| 11 | 9, 10 | bitr4i 278 |
. . . . . . . 8
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ ∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
| 12 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
| 13 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉) |
| 14 | 12, 13 | anim12i 613 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
| 15 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
| 16 | | s3cli 14920 |
. . . . . . . . . . . . . 14
⊢
〈“𝑎𝑏𝑐”〉 ∈ Word V |
| 17 | 15, 16 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ V ∧
〈“𝑎𝑏𝑐”〉 ∈ Word V) |
| 18 | 1 | isspthonpth 29769 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑓 ∈ V ∧ 〈“𝑎𝑏𝑐”〉 ∈ Word V)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ↔ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐))) |
| 19 | 14, 17, 18 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ↔ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐))) |
| 20 | | wwlknon 29877 |
. . . . . . . . . . . . 13
⊢
(〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) |
| 21 | | 2nn0 12543 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
| 22 | | iswwlksn 29858 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℕ0 → (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)))) |
| 23 | 21, 22 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)))) |
| 24 | 23 | 3anbi1d 1442 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) ↔ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
| 25 | 20, 24 | bitrid 283 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
| 26 | 19, 25 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
| 27 | 26 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
| 28 | 16 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 〈“𝑎𝑏𝑐”〉 ∈ Word V) |
| 29 | | simprl1 1219 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉) |
| 30 | | spthiswlk 29746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 → 𝑓(Walks‘𝐺)〈“𝑎𝑏𝑐”〉) |
| 31 | | wlklenvm1 29640 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(Walks‘𝐺)〈“𝑎𝑏𝑐”〉 → (♯‘𝑓) =
((♯‘〈“𝑎𝑏𝑐”〉) − 1)) |
| 32 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑓)
= ((♯‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (♯‘𝑓) = ((♯‘〈“𝑎𝑏𝑐”〉) − 1)) |
| 33 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1) →
((♯‘〈“𝑎𝑏𝑐”〉) − 1) = ((2 + 1) −
1)) |
| 34 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℂ |
| 35 | | pncan1 11687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (2 ∈
ℂ → ((2 + 1) − 1) = 2) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2 + 1)
− 1) = 2 |
| 37 | 33, 36 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1) →
((♯‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) →
((♯‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
| 39 | 38 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → ((♯‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑓)
= ((♯‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → ((♯‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
| 41 | 32, 40 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝑓)
= ((♯‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (♯‘𝑓) = 2) |
| 42 | 41 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑓) =
((♯‘〈“𝑎𝑏𝑐”〉) − 1) →
(((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (♯‘𝑓) = 2)) |
| 43 | 30, 31, 42 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 → (((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (♯‘𝑓) = 2)) |
| 44 | 43 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) → (((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (♯‘𝑓) = 2)) |
| 45 | 44 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (♯‘𝑓) = 2) |
| 46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (♯‘𝑓) = 2) |
| 47 | | s3fv0 14930 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ V →
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎) |
| 48 | 47 | elv 3485 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 |
| 49 | 48 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑎 = (〈“𝑎𝑏𝑐”〉‘0) |
| 50 | | s3fv1 14931 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ V →
(〈“𝑎𝑏𝑐”〉‘1) = 𝑏) |
| 51 | 50 | elv 3485 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘1) = 𝑏 |
| 52 | 51 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) |
| 53 | | s3fv2 14932 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ V →
(〈“𝑎𝑏𝑐”〉‘2) = 𝑐) |
| 54 | 53 | elv 3485 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘2) = 𝑐 |
| 55 | 54 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2) |
| 56 | 49, 52, 55 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)) |
| 57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))) |
| 58 | 29, 46, 57 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)))) |
| 59 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑓(SPaths‘𝐺)𝑝 ↔ 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉)) |
| 60 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘0) = (〈“𝑎𝑏𝑐”〉‘0)) |
| 61 | 60 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑎 = (𝑝‘0) ↔ 𝑎 = (〈“𝑎𝑏𝑐”〉‘0))) |
| 62 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘1) = (〈“𝑎𝑏𝑐”〉‘1)) |
| 63 | 62 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑏 = (𝑝‘1) ↔ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1))) |
| 64 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘2) = (〈“𝑎𝑏𝑐”〉‘2)) |
| 65 | 64 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑐 = (𝑝‘2) ↔ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))) |
| 66 | 61, 63, 65 | 3anbi123d 1438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)))) |
| 67 | 59, 66 | 3anbi13d 1440 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))))) |
| 68 | 67 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))))) |
| 69 | 58, 68 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) |
| 70 | 69 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 71 | 28, 70 | spcimedv 3595 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 72 | | spthiswlk 29746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝) |
| 73 | | wlklenvp1 29636 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1)) |
| 74 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = (2 + 1)) |
| 75 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 + 1) =
3 |
| 76 | 74, 75 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = 3) |
| 77 | 76 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑓) =
2 → ((♯‘𝑝)
= ((♯‘𝑓) + 1)
↔ (♯‘𝑝) =
3)) |
| 78 | 77 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑝) =
((♯‘𝑓) + 1)
→ ((♯‘𝑓) =
2 → (♯‘𝑝)
= 3)) |
| 79 | 72, 73, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPaths‘𝐺)𝑝 → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3)) |
| 80 | 79 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = 3) |
| 81 | 80 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (♯‘𝑝) = 3) |
| 82 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (♯‘𝑝) = 3) |
| 83 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎) |
| 84 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏) |
| 85 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐) |
| 86 | 83, 84, 85 | 3anbi123i 1156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
| 87 | 86 | biimpi 216 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
| 88 | 87 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
| 89 | 88 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
| 90 | 82, 89 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))) |
| 91 | 1 | wlkpwrd 29635 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
| 92 | 72, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
| 93 | 92 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉) |
| 94 | 12 | anim1i 615 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
| 95 | | 3anass 1095 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
| 96 | 94, 95 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
| 97 | | eqwrds3 15000 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
| 98 | 93, 96, 97 | syl2anr 597 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
| 99 | 90, 98 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 = 〈“𝑎𝑏𝑐”〉) |
| 100 | 59 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPaths‘𝐺)𝑝 → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉)) |
| 101 | 100 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉)) |
| 102 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉)) |
| 103 | 102 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉) |
| 104 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘0) = 𝑎) |
| 105 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑓) =
2 → (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = (〈“𝑎𝑏𝑐”〉‘2)) |
| 106 | 105, 54 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑓) =
2 → (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) |
| 107 | 106 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) |
| 108 | 107 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) |
| 109 | 103, 104,
108 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐)) |
| 110 | | wlkiswwlks1 29887 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ∈ UPGraph → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺))) |
| 111 | 110 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺))) |
| 112 | 111 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺))) |
| 113 | 72, 112 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(SPaths‘𝐺)𝑝 → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalks‘𝐺))) |
| 114 | 113 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalks‘𝐺))) |
| 115 | 114 | impcom 407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 ∈ (WWalks‘𝐺)) |
| 116 | 115 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑝 ∈ (WWalks‘𝐺)) |
| 117 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝 ∈ (WWalks‘𝐺) ↔ 〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺))) |
| 118 | 117 | bicomd 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ↔ 𝑝 ∈ (WWalks‘𝐺))) |
| 119 | 118 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ↔ 𝑝 ∈ (WWalks‘𝐺))) |
| 120 | 116, 119 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺)) |
| 121 | | s3len 14933 |
. . . . . . . . . . . . . . . . . . 19
⊢
(♯‘〈“𝑎𝑏𝑐”〉) = 3 |
| 122 | | df-3 12330 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 = (2 +
1) |
| 123 | 121, 122 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1) |
| 124 | 120, 123 | jctir 520 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1))) |
| 125 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) |
| 126 | 124, 104,
125 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) |
| 127 | 109, 126 | jca 511 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
| 128 | 99, 127 | mpdan 687 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
| 129 | 128 | ex 412 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
| 130 | 129 | exlimdv 1933 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
| 131 | 71, 130 | impbid 212 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 132 | 131 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 133 | 27, 132 | bitrd 279 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 134 | 133 | exbidv 1921 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 135 | 11, 134 | bitrid 283 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 136 | 8, 135 | bitrid 283 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
| 137 | 136 | pm5.32da 579 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
| 138 | 137 | 2rexbidva 3220 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
| 139 | 7, 138 | bitrid 283 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
| 140 | 139 | rexbidva 3177 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
| 141 | 3, 6, 140 | 3bitrd 305 |
1
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |