Metamath Proof Explorer

Theorem iswspthn

Description: An element of the set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 11-May-2021)

Ref Expression
Assertion iswspthn ⊢ W ∈ N WSPathsN G ↔ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W

Proof

Step Hyp Ref Expression
1 breq2 ⊢ w = W → f SPaths ⁡ G w ↔ f SPaths ⁡ G W
2 1 exbidv ⊢ w = W → ∃ f f SPaths ⁡ G w ↔ ∃ f f SPaths ⁡ G W
3 wspthsn ⊢ N WSPathsN G = w ∈ N WWalksN G | ∃ f f SPaths ⁡ G w
4 2 3 elrab2 ⊢ W ∈ N WSPathsN G ↔ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W