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 | ⊢ ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | breq2 | ⊢ ( 𝑤 = 𝑊 → ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ↔ 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ) | |
| 2 | 1 | exbidv | ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ↔ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ) |
| 3 | wspthsn | ⊢ ( 𝑁 WSPathsN 𝐺 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } | |
| 4 | 2 3 | elrab2 | ⊢ ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ) |