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 WANWSPathsNOnGBWANWWalksNOnGBffASPathsOnGBW

Proof

Step Hyp Ref Expression
1 breq2 w=WfASPathsOnGBwfASPathsOnGBW
2 1 exbidv w=WffASPathsOnGBwffASPathsOnGBW
3 eqid VtxG=VtxG
4 3 iswspthsnon ANWSPathsNOnGB=wANWWalksNOnGB|ffASPathsOnGBw
5 2 4 elrab2 WANWSPathsNOnGBWANWWalksNOnGBffASPathsOnGBW