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 ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ↔ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )

Proof

Step Hyp Ref Expression
1 breq2 ( 𝑤 = 𝑊 → ( 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )
2 1 exbidv ( 𝑤 = 𝑊 → ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )
3 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 3 iswspthsnon ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 }
5 2 4 elrab2 ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ↔ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )