Description: In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | upgr1wlkd.p | |- P = <" X Y "> |
|
upgr1wlkd.f | |- F = <" J "> |
||
upgr1wlkd.x | |- ( ph -> X e. ( Vtx ` G ) ) |
||
upgr1wlkd.y | |- ( ph -> Y e. ( Vtx ` G ) ) |
||
upgr1wlkd.j | |- ( ph -> ( ( iEdg ` G ) ` J ) = { X , Y } ) |
||
upgr1wlkd.g | |- ( ph -> G e. UPGraph ) |
||
Assertion | upgr1trld | |- ( ph -> F ( Trails ` G ) P ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | upgr1wlkd.p | |- P = <" X Y "> |
|
2 | upgr1wlkd.f | |- F = <" J "> |
|
3 | upgr1wlkd.x | |- ( ph -> X e. ( Vtx ` G ) ) |
|
4 | upgr1wlkd.y | |- ( ph -> Y e. ( Vtx ` G ) ) |
|
5 | upgr1wlkd.j | |- ( ph -> ( ( iEdg ` G ) ` J ) = { X , Y } ) |
|
6 | upgr1wlkd.g | |- ( ph -> G e. UPGraph ) |
|
7 | 1 2 3 4 5 | upgr1wlkdlem1 | |- ( ( ph /\ X = Y ) -> ( ( iEdg ` G ) ` J ) = { X } ) |
8 | 1 2 3 4 5 | upgr1wlkdlem2 | |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( ( iEdg ` G ) ` J ) ) |
9 | eqid | |- ( Vtx ` G ) = ( Vtx ` G ) |
|
10 | eqid | |- ( iEdg ` G ) = ( iEdg ` G ) |
|
11 | 1 2 3 4 7 8 9 10 | 1trld | |- ( ph -> F ( Trails ` G ) P ) |