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 ∈ A N WSPathsNOn G B ↔ W ∈ A N WWalksNOn G B ∧ ∃ 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 → ∃ f f A SPathsOn ⁡ G B w ↔ ∃ f f A SPathsOn ⁡ G B W
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 iswspthsnon ⊢ A N WSPathsNOn G B = w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w
5 2 4 elrab2 ⊢ W ∈ A N WSPathsNOn G B ↔ W ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B W