Metamath Proof Explorer


Theorem wspthnon

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 ) )

Proof

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 ) )