Description: An element of the set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 12-May-2021) (Revised by AV, 15-Mar-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wspthnon | |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | breq2 | |- ( w = W -> ( f ( A ( SPathsOn ` G ) B ) w <-> f ( A ( SPathsOn ` G ) B ) W ) ) |
|
| 2 | 1 | exbidv | |- ( w = W -> ( E. f f ( A ( SPathsOn ` G ) B ) w <-> E. f f ( A ( SPathsOn ` G ) B ) W ) ) |
| 3 | eqid | |- ( Vtx ` G ) = ( Vtx ` G ) |
|
| 4 | 3 | iswspthsnon | |- ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } |
| 5 | 2 4 | elrab2 | |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) ) |