Proof of Theorem elwspths2spth
Step | Hyp | Ref
| Expression |
1 | | elwwlks2.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | wspthsnwspthsnon 27203 |
. . 3
⊢ (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) |
3 | 2 | a1i 11 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))) |
4 | 1 | elwspths2on 27250 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
5 | 4 | 3expb 1150 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
6 | 5 | 2rexbidva 3237 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
7 | | rexcom 3280 |
. . . 4
⊢
(∃𝑐 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))) |
8 | | wspthnon 27112 |
. . . . . . 7
⊢
(〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉)) |
9 | | ancom 453 |
. . . . . . . . 9
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
10 | | 19.41v 2045 |
. . . . . . . . 9
⊢
(∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
11 | 9, 10 | bitr4i 270 |
. . . . . . . 8
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ ∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
12 | | simpr 478 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
13 | | simpr 478 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉) |
14 | 12, 13 | anim12i 607 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
15 | | vex 3388 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
16 | | s3cli 13966 |
. . . . . . . . . . . . . 14
⊢
〈“𝑎𝑏𝑐”〉 ∈ Word V |
17 | 15, 16 | pm3.2i 463 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ V ∧
〈“𝑎𝑏𝑐”〉 ∈ Word V) |
18 | 1 | isspthonpth 27003 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑓 ∈ V ∧ 〈“𝑎𝑏𝑐”〉 ∈ Word V)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ↔ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐))) |
19 | 14, 17, 18 | sylancl 581 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ↔ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐))) |
20 | | wwlknon 27111 |
. . . . . . . . . . . . 13
⊢
(〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) |
21 | | 2nn0 11599 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 |
22 | | iswwlksn 27089 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ0 → (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)))) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1))) |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)))) |
25 | 24 | 3anbi1d 1565 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) ↔ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
26 | 20, 25 | syl5bb 275 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
27 | 19, 26 | anbi12d 625 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
28 | 27 | adantr 473 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
29 | 16 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 〈“𝑎𝑏𝑐”〉 ∈ Word V) |
30 | | simprl1 1282 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉) |
31 | | spthiswlk 26982 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 → 𝑓(Walks‘𝐺)〈“𝑎𝑏𝑐”〉) |
32 | | wlklenvm1 26871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(Walks‘𝐺)〈“𝑎𝑏𝑐”〉 → (♯‘𝑓) =
((♯‘〈“𝑎𝑏𝑐”〉) − 1)) |
33 | | simpl 475 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑓)
= ((♯‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (♯‘𝑓) = ((♯‘〈“𝑎𝑏𝑐”〉) − 1)) |
34 | | oveq1 6885 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1) →
((♯‘〈“𝑎𝑏𝑐”〉) − 1) = ((2 + 1) −
1)) |
35 | | 2cn 11388 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℂ |
36 | | pncan1 10746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (2 ∈
ℂ → ((2 + 1) − 1) = 2) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2 + 1)
− 1) = 2 |
38 | 34, 37 | syl6eq 2849 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1) →
((♯‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
39 | 38 | adantl 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) →
((♯‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
40 | 39 | 3ad2ant1 1164 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → ((♯‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
41 | 40 | adantl 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑓)
= ((♯‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → ((♯‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
42 | 33, 41 | eqtrd 2833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝑓)
= ((♯‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (♯‘𝑓) = 2) |
43 | 42 | ex 402 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑓) =
((♯‘〈“𝑎𝑏𝑐”〉) − 1) →
(((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (♯‘𝑓) = 2)) |
44 | 31, 32, 43 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 → (((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (♯‘𝑓) = 2)) |
45 | 44 | 3ad2ant1 1164 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) → (((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (♯‘𝑓) = 2)) |
46 | 45 | imp 396 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (♯‘𝑓) = 2) |
47 | 46 | adantl 474 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (♯‘𝑓) = 2) |
48 | | vex 3388 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑎 ∈ V |
49 | | s3fv0 13976 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ V →
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 |
51 | 50 | eqcomi 2808 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑎 = (〈“𝑎𝑏𝑐”〉‘0) |
52 | | vex 3388 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑏 ∈ V |
53 | | s3fv1 13977 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ V →
(〈“𝑎𝑏𝑐”〉‘1) = 𝑏) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘1) = 𝑏 |
55 | 54 | eqcomi 2808 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) |
56 | | vex 3388 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑐 ∈ V |
57 | | s3fv2 13978 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ V →
(〈“𝑎𝑏𝑐”〉‘2) = 𝑐) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘2) = 𝑐 |
59 | 58 | eqcomi 2808 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2) |
60 | 51, 55, 59 | 3pm3.2i 1439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)) |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))) |
62 | 30, 47, 61 | 3jca 1159 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)))) |
63 | | breq2 4847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑓(SPaths‘𝐺)𝑝 ↔ 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉)) |
64 | | fveq1 6410 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘0) = (〈“𝑎𝑏𝑐”〉‘0)) |
65 | 64 | eqeq2d 2809 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑎 = (𝑝‘0) ↔ 𝑎 = (〈“𝑎𝑏𝑐”〉‘0))) |
66 | | fveq1 6410 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘1) = (〈“𝑎𝑏𝑐”〉‘1)) |
67 | 66 | eqeq2d 2809 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑏 = (𝑝‘1) ↔ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1))) |
68 | | fveq1 6410 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘2) = (〈“𝑎𝑏𝑐”〉‘2)) |
69 | 68 | eqeq2d 2809 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑐 = (𝑝‘2) ↔ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))) |
70 | 65, 67, 69 | 3anbi123d 1561 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)))) |
71 | 63, 70 | 3anbi13d 1563 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))))) |
72 | 71 | ad2antlr 719 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))))) |
73 | 62, 72 | mpbird 249 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) |
74 | 73 | ex 402 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
75 | 29, 74 | spcimedv 3480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
76 | | spthiswlk 26982 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝) |
77 | | wlklenvp1 26868 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1)) |
78 | | oveq1 6885 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = (2 + 1)) |
79 | | 2p1e3 11462 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 + 1) =
3 |
80 | 78, 79 | syl6eq 2849 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = 3) |
81 | 80 | eqeq2d 2809 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑓) =
2 → ((♯‘𝑝)
= ((♯‘𝑓) + 1)
↔ (♯‘𝑝) =
3)) |
82 | 81 | biimpcd 241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑝) =
((♯‘𝑓) + 1)
→ ((♯‘𝑓) =
2 → (♯‘𝑝)
= 3)) |
83 | 76, 77, 82 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPaths‘𝐺)𝑝 → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3)) |
84 | 83 | imp 396 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = 3) |
85 | 84 | 3adant3 1163 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (♯‘𝑝) = 3) |
86 | 85 | adantl 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (♯‘𝑝) = 3) |
87 | | eqcom 2806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎) |
88 | | eqcom 2806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏) |
89 | | eqcom 2806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐) |
90 | 87, 88, 89 | 3anbi123i 1195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
91 | 90 | biimpi 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
92 | 91 | 3ad2ant3 1166 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
93 | 92 | adantl 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
94 | 86, 93 | jca 508 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))) |
95 | 1 | wlkpwrd 26867 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
96 | 76, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
97 | 96 | 3ad2ant1 1164 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉) |
98 | 12 | anim1i 609 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
99 | | 3anass 1117 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
100 | 98, 99 | sylibr 226 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
101 | | eqwrds3 14047 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
102 | 97, 100, 101 | syl2anr 591 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
103 | 94, 102 | mpbird 249 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 = 〈“𝑎𝑏𝑐”〉) |
104 | 63 | biimpcd 241 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPaths‘𝐺)𝑝 → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉)) |
105 | 104 | 3ad2ant1 1164 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉)) |
106 | 105 | adantl 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉)) |
107 | 106 | imp 396 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉) |
108 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘0) = 𝑎) |
109 | | fveq2 6411 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑓) =
2 → (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = (〈“𝑎𝑏𝑐”〉‘2)) |
110 | 109, 58 | syl6eq 2849 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑓) =
2 → (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) |
111 | 110 | 3ad2ant2 1165 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) |
112 | 111 | ad2antlr 719 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) |
113 | 107, 108,
112 | 3jca 1159 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐)) |
114 | | wlkiswwlks1 27124 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ∈ UPGraph → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺))) |
115 | 114 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺))) |
116 | 115 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺))) |
117 | 76, 116 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(SPaths‘𝐺)𝑝 → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalks‘𝐺))) |
118 | 117 | 3ad2ant1 1164 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalks‘𝐺))) |
119 | 118 | impcom 397 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 ∈ (WWalks‘𝐺)) |
120 | 119 | adantr 473 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑝 ∈ (WWalks‘𝐺)) |
121 | | eleq1 2866 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝 ∈ (WWalks‘𝐺) ↔ 〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺))) |
122 | 121 | bicomd 215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ↔ 𝑝 ∈ (WWalks‘𝐺))) |
123 | 122 | adantl 474 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ↔ 𝑝 ∈ (WWalks‘𝐺))) |
124 | 120, 123 | mpbird 249 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺)) |
125 | | s3len 13979 |
. . . . . . . . . . . . . . . . . . 19
⊢
(♯‘〈“𝑎𝑏𝑐”〉) = 3 |
126 | | df-3 11377 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 = (2 +
1) |
127 | 125, 126 | eqtri 2821 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1) |
128 | 124, 127 | jctir 517 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1))) |
129 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) |
130 | 128, 108,
129 | 3jca 1159 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) |
131 | 113, 130 | jca 508 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
132 | 103, 131 | mpdan 679 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
133 | 132 | ex 402 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
134 | 133 | exlimdv 2029 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
135 | 75, 134 | impbid 204 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
136 | 135 | adantr 473 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (((𝑓(SPaths‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(♯‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalks‘𝐺) ∧
(♯‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
137 | 28, 136 | bitrd 271 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
138 | 137 | exbidv 2017 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
139 | 11, 138 | syl5bb 275 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
140 | 8, 139 | syl5bb 275 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
141 | 140 | pm5.32da 575 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
142 | 141 | 2rexbidva 3237 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
143 | 7, 142 | syl5bb 275 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
144 | 143 | rexbidva 3230 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
145 | 3, 6, 144 | 3bitrd 297 |
1
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |