Proof of Theorem elwspths2spth
Step | Hyp | Ref
| Expression |
1 | | 2nn0 11186 |
. . 3
⊢ 2 ∈
ℕ0 |
2 | | elwwlks2.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
3 | 2 | wspthsnwspthsnon 41122 |
. . 3
⊢ ((2
∈ ℕ0 ∧ 𝐺 ∈ UPGraph ) → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))) |
4 | 1, 3 | mpan 702 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))) |
5 | 2 | elwspths2on 41163 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
6 | 5 | 3expb 1258 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
7 | 6 | 2rexbidva 3038 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))) |
8 | | rexcom 3080 |
. . . 4
⊢
(∃𝑐 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))) |
9 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
10 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉) |
11 | 9, 10 | anim12i 588 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
12 | 2 | wspthnon 41054 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉))) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉))) |
14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉))) |
15 | | ancom 465 |
. . . . . . . . 9
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
16 | | 19.41v 1901 |
. . . . . . . . 9
⊢
(∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
17 | 15, 16 | bitr4i 266 |
. . . . . . . 8
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ ∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))) |
18 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
19 | | s3cli 13476 |
. . . . . . . . . . . . . 14
⊢
〈“𝑎𝑏𝑐”〉 ∈ Word V |
20 | 18, 19 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ V ∧
〈“𝑎𝑏𝑐”〉 ∈ Word V) |
21 | 2 | isspthonpth-av 40955 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑓 ∈ V ∧ 〈“𝑎𝑏𝑐”〉 ∈ Word V)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ↔ (𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐))) |
22 | 11, 20, 21 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ↔ (𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐))) |
23 | 2 | wwlknon 41053 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalkSN 𝐺) ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
24 | 11, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalkSN 𝐺) ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
25 | | iswwlksn 41041 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ0 → (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalkSN 𝐺) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)))) |
26 | 1, 25 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(〈“𝑎𝑏𝑐”〉 ∈ (2 WWalkSN 𝐺) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1))) |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (〈“𝑎𝑏𝑐”〉 ∈ (2 WWalkSN 𝐺) ↔ (〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)))) |
28 | 27 | 3anbi1d 1395 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((〈“𝑎𝑏𝑐”〉 ∈ (2 WWalkSN 𝐺) ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) ↔ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
29 | 24, 28 | bitrd 267 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
30 | 22, 29 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
31 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
32 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 〈“𝑎𝑏𝑐”〉 ∈ Word V) |
33 | | simprl1 1099 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → 𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉) |
34 | | sPthis1wlk 40934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 → 𝑓(1Walks‘𝐺)〈“𝑎𝑏𝑐”〉) |
35 | | 1wlklenvm1 40826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(1Walks‘𝐺)〈“𝑎𝑏𝑐”〉 → (#‘𝑓) = ((#‘〈“𝑎𝑏𝑐”〉) − 1)) |
36 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑓) =
((#‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (#‘𝑓) = ((#‘〈“𝑎𝑏𝑐”〉) − 1)) |
37 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘〈“𝑎𝑏𝑐”〉) = (2 + 1) →
((#‘〈“𝑎𝑏𝑐”〉) − 1) = ((2 + 1) −
1)) |
38 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℂ |
39 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (2 ∈
ℂ → ((2 + 1) − 1) = 2) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2 + 1)
− 1) = 2 |
41 | 37, 40 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘〈“𝑎𝑏𝑐”〉) = (2 + 1) →
((#‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) →
((#‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
43 | 42 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → ((#‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑓) =
((#‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → ((#‘〈“𝑎𝑏𝑐”〉) − 1) =
2) |
45 | 36, 44 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑓) =
((#‘〈“𝑎𝑏𝑐”〉) − 1) ∧
((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (#‘𝑓) = 2) |
46 | 45 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑓) =
((#‘〈“𝑎𝑏𝑐”〉) − 1) →
(((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (#‘𝑓) = 2)) |
47 | 34, 35, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 → (((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (#‘𝑓) = 2)) |
48 | 47 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) → (((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) → (#‘𝑓) = 2)) |
49 | 48 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (#‘𝑓) = 2) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (#‘𝑓) = 2) |
51 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑎 ∈ V |
52 | | s3fv0 13486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ V →
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 |
54 | 53 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑎 = (〈“𝑎𝑏𝑐”〉‘0) |
55 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑏 ∈ V |
56 | | s3fv1 13487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ V →
(〈“𝑎𝑏𝑐”〉‘1) = 𝑏) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘1) = 𝑏 |
58 | 57 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) |
59 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑐 ∈ V |
60 | | s3fv2 13488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ V →
(〈“𝑎𝑏𝑐”〉‘2) = 𝑐) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈“𝑎𝑏𝑐”〉‘2) = 𝑐 |
62 | 61 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2) |
63 | 54, 58, 62 | 3pm3.2i 1232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)) |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))) |
65 | 33, 50, 64 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)))) |
66 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑓(SPathS‘𝐺)𝑝 ↔ 𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉)) |
67 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘0) = (〈“𝑎𝑏𝑐”〉‘0)) |
68 | 67 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑎 = (𝑝‘0) ↔ 𝑎 = (〈“𝑎𝑏𝑐”〉‘0))) |
69 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘1) = (〈“𝑎𝑏𝑐”〉‘1)) |
70 | 69 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑏 = (𝑝‘1) ↔ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1))) |
71 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝‘2) = (〈“𝑎𝑏𝑐”〉‘2)) |
72 | 71 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑐 = (𝑝‘2) ↔ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))) |
73 | 68, 70, 72 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2)))) |
74 | 66, 73 | 3anbi13d 1393 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))))) |
75 | 74 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (〈“𝑎𝑏𝑐”〉‘0) ∧ 𝑏 = (〈“𝑎𝑏𝑐”〉‘1) ∧ 𝑐 = (〈“𝑎𝑏𝑐”〉‘2))))) |
76 | 65, 75 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) ∧ ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) → (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) |
77 | 76 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
78 | 32, 77 | spcimedv 3265 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) → ∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
79 | | sPthis1wlk 40934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(SPathS‘𝐺)𝑝 → 𝑓(1Walks‘𝐺)𝑝) |
80 | | 1wlklenvp1 40823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(1Walks‘𝐺)𝑝 → (#‘𝑝) = ((#‘𝑓) + 1)) |
81 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑓) = 2
→ ((#‘𝑓) + 1) =
(2 + 1)) |
82 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 + 1) =
3 |
83 | 81, 82 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑓) = 2
→ ((#‘𝑓) + 1) =
3) |
84 | 83 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑓) = 2
→ ((#‘𝑝) =
((#‘𝑓) + 1) ↔
(#‘𝑝) =
3)) |
85 | 84 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) =
((#‘𝑓) + 1) →
((#‘𝑓) = 2 →
(#‘𝑝) =
3)) |
86 | 79, 80, 85 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPathS‘𝐺)𝑝 → ((#‘𝑓) = 2 → (#‘𝑝) = 3)) |
87 | 86 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2) → (#‘𝑝) = 3) |
88 | 87 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (#‘𝑝) = 3) |
89 | 88 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (#‘𝑝) = 3) |
90 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎) |
91 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏) |
92 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐) |
93 | 90, 91, 92 | 3anbi123i 1244 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
94 | 93 | biimpi 205 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
95 | 94 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)) |
97 | 89, 96 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))) |
98 | 2 | 1wlkpwrd 40822 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓(1Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
99 | 79, 98 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓(SPathS‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
100 | 99 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉) |
101 | 9 | anim1i 590 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
102 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) |
103 | 101, 102 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) |
104 | | eqwrds3 13552 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
105 | 100, 103,
104 | syl2anr 494 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 ↔ ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))) |
106 | 97, 105 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 = 〈“𝑎𝑏𝑐”〉) |
107 | 66 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(SPathS‘𝐺)𝑝 → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉)) |
108 | 107 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉)) |
109 | 108 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = 〈“𝑎𝑏𝑐”〉 → 𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉)) |
110 | 109 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉) |
111 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘0) = 𝑎) |
112 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑓) = 2
→ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = (〈“𝑎𝑏𝑐”〉‘2)) |
113 | 112, 61 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑓) = 2
→ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) |
114 | 113 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) |
115 | 114 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) |
116 | 110, 111,
115 | 3jca 1235 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐)) |
117 | | 1wlkiswwlks1 41064 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ∈ UPGraph → (𝑓(1Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalkS‘𝐺))) |
118 | 117 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (𝑓(1Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalkS‘𝐺))) |
119 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(1Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalkS‘𝐺))) |
120 | 79, 119 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(SPathS‘𝐺)𝑝 → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalkS‘𝐺))) |
121 | 120 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalkS‘𝐺))) |
122 | 121 | impcom 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 ∈ (WWalkS‘𝐺)) |
123 | 122 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 𝑝 ∈ (WWalkS‘𝐺)) |
124 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (𝑝 ∈ (WWalkS‘𝐺) ↔ 〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺))) |
125 | 124 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 〈“𝑎𝑏𝑐”〉 → (〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ↔ 𝑝 ∈ (WWalkS‘𝐺))) |
126 | 125 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ↔ 𝑝 ∈ (WWalkS‘𝐺))) |
127 | 123, 126 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → 〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺)) |
128 | | s3len 13489 |
. . . . . . . . . . . . . . . . . . 19
⊢
(#‘〈“𝑎𝑏𝑐”〉) = 3 |
129 | | df-3 10957 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 = (2 +
1) |
130 | 128, 129 | eqtri 2632 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1) |
131 | 127, 130 | jctir 559 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1))) |
132 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉‘2) = 𝑐) |
133 | 131, 111,
132 | 3jca 1235 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) |
134 | 116, 133 | jca 553 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑎 ∈
𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
135 | 106, 134 | mpdan 699 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐))) |
136 | 135 | ex 449 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
137 | 136 | exlimdv 1848 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)))) |
138 | 78, 137 | impbid 201 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) ↔ ∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
139 | 138 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (((𝑓(SPathS‘𝐺)〈“𝑎𝑏𝑐”〉 ∧ (〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘(#‘𝑓)) = 𝑐) ∧ ((〈“𝑎𝑏𝑐”〉 ∈ (WWalkS‘𝐺) ∧
(#‘〈“𝑎𝑏𝑐”〉) = (2 + 1)) ∧
(〈“𝑎𝑏𝑐”〉‘0) = 𝑎 ∧ (〈“𝑎𝑏𝑐”〉‘2) = 𝑐)) ↔ ∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
140 | 31, 139 | bitrd 267 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
141 | 140 | exbidv 1837 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑓∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
142 | 17, 141 | syl5bb 271 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → ((〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)〈“𝑎𝑏𝑐”〉) ↔ ∃𝑓∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
143 | 14, 142 | bitrd 267 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = 〈“𝑎𝑏𝑐”〉) → (〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑓∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))) |
144 | 143 | pm5.32da 671 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
145 | 144 | 2rexbidva 3038 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
146 | 8, 145 | syl5bb 271 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
147 | 146 | rexbidva 3031 |
. 2
⊢ (𝐺 ∈ UPGraph →
(∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ 〈“𝑎𝑏𝑐”〉 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |
148 | 4, 7, 147 | 3bitrd 293 |
1
⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPathS‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) |