Description: In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | upgr1wlkd.p | ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩ | |
| upgr1wlkd.f | ⊢ 𝐹 = ⟨“ 𝐽 ”⟩ | ||
| upgr1wlkd.x | ⊢ ( 𝜑 → 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) | ||
| upgr1wlkd.y | ⊢ ( 𝜑 → 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) | ||
| upgr1wlkd.j | ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } ) | ||
| upgr1wlkd.g | ⊢ ( 𝜑 → 𝐺 ∈ UPGraph ) | ||
| Assertion | upgr1wlkd | ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | upgr1wlkd.p | ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩ | |
| 2 | upgr1wlkd.f | ⊢ 𝐹 = ⟨“ 𝐽 ”⟩ | |
| 3 | upgr1wlkd.x | ⊢ ( 𝜑 → 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) | |
| 4 | upgr1wlkd.y | ⊢ ( 𝜑 → 𝑌 ∈ ( Vtx ‘ 𝐺 ) ) | |
| 5 | upgr1wlkd.j | ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } ) | |
| 6 | upgr1wlkd.g | ⊢ ( 𝜑 → 𝐺 ∈ UPGraph ) | |
| 7 | 1 2 3 4 5 | upgr1wlkdlem1 | ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 } ) |
| 8 | 1 2 3 4 5 | upgr1wlkdlem2 | ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) ) |
| 9 | eqid | ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) | |
| 10 | eqid | ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) | |
| 11 | 1 2 3 4 7 8 9 10 | 1wlkd | ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) |