P. 297 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29601-29700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wlkp1lem1 29601	Lemma for wlkp1 29609. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    ⇒   ⊢ (𝜑 → ¬ (𝑁 + 1) ∈ dom 𝑃)
Theorem	wlkp1lem2 29602	Lemma for wlkp1 29609. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    ⇒   ⊢ (𝜑 → (♯‘𝐻) = (𝑁 + 1))
Theorem	wlkp1lem3 29603	Lemma for wlkp1 29609. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    ⇒   ⊢ (𝜑 → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘𝐵))
Theorem	wlkp1lem4 29604	Lemma for wlkp1 29609. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
Theorem	wlkp1lem5 29605*	Lemma for wlkp1 29609. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)(𝑄‘𝑘) = (𝑃‘𝑘))
Theorem	wlkp1lem6 29606*	Lemma for wlkp1 29609. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))))
Theorem	wlkp1lem7 29607	Lemma for wlkp1 29609. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))
Theorem	wlkp1lem8 29608*	Lemma for wlkp1 29609. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))
Theorem	wlkp1 29609	Append one path segment (edge) 𝐸 from vertex (𝑃‘𝑁) to a vertex 𝐶 to a walk ⟨𝐹, 𝑃⟩ to become a walk ⟨𝐻, 𝑄⟩ of the supergraph 𝑆 obtained by adding the new edge to the graph 𝐺. Formerly proven directly for Eulerian paths (for pseudographs), see eupthp1 30145. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 6-Mar-2021.) (Proof shortened by AV, 18-Apr-2021.) (Revised by AV, 8-Apr-2024.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})    ⇒   ⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄)
Theorem	wlkdlem1 29610*	Lemma 1 for wlkd 29614. (Contributed by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	wlkdlem2 29611*	Lemma 2 for wlkd 29614. (Contributed by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → (((♯‘𝐹) ∈ ℕ → (𝑃‘(♯‘𝐹)) ∈ (𝐼‘(𝐹‘((♯‘𝐹) − 1)))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘))))
Theorem	wlkdlem3 29612*	Lemma 3 for wlkd 29614. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
Theorem	wlkdlem4 29613*	Lemma 4 for wlkd 29614. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 23-Jan-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
Theorem	wlkd 29614*	Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
17.3.2  Walks for loop-free graphs
Theorem	lfgrwlkprop 29615*	Two adjacent vertices in a walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
Theorem	lfgriswlk 29616*	Conditions for a pair of functions to be a walk in a loop-free graph. (Contributed by AV, 28-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
Theorem	lfgrwlknloop 29617*	In a loop-free graph, each walk has no loops! (Contributed by AV, 2-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
17.3.3  Trails
Syntax	ctrls 29618	Extend class notation with trails (within a graph).
class Trails
Syntax	ctrlson 29619	Extend class notation with trails between two vertices (within a graph).
class TrailsOn
Definition	df-trls 29620*	Define the set of all Trails (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A trail is a walk in which all edges are distinct. According to Bollobas: "... walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5. Therefore, a trail can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the trail is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ Trails = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ Fun ◡𝑓)})
Definition	df-trlson 29621*	Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ TrailsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Trails‘𝑔)𝑝)}))
Theorem	reltrls 29622	The set (Trails‘𝐺) of all trails on 𝐺 is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021.)
⊢ Rel (Trails‘𝐺)
Theorem	trlsfval 29623*	The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)
⊢ (Trails‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ◡𝑓)}
Theorem	istrl 29624	Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)
⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹))
Theorem	trliswlk 29625	A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 29-Oct-2021.)
⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	trlf1 29626	The enumeration 𝐹 of a trail ⟨𝐹, 𝑃⟩ is injective. (Contributed by AV, 20-Feb-2021.) (Proof shortened by AV, 29-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼)
Theorem	trlreslem 29627	Lemma for trlres 29628. Formerly part of proof of eupthres 30144. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ 𝐻 = (𝐹 prefix 𝑁)    ⇒   ⊢ (𝜑 → 𝐻:(0..^(♯‘𝐻))–1-1-onto→dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
Theorem	trlres 29628	The restriction ⟨𝐻, 𝑄⟩ of a trail ⟨𝐹, 𝑃⟩ to an initial segment of the trail (of length 𝑁) forms a trail on the subgraph 𝑆 consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ 𝐻 = (𝐹 prefix 𝑁)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))    ⇒   ⊢ (𝜑 → 𝐻(Trails‘𝑆)𝑄)
Theorem	upgrtrls 29629*	The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (Trails‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ ((𝑓 ∈ Word dom 𝐼 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})
Theorem	upgristrl 29630*	Properties of a pair of functions to be a trail in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (𝐹(Trails‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
Theorem	upgrf1istrl 29631*	Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
Theorem	wksonproplem 29632*	Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop 29636. (Contributed by AV, 16-Jan-2021.) Remove is-walk hypothesis. (Revised by SN, 13-Dec-2024.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃)))    &   ⊢ 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑂‘𝑔)𝑏)𝑝 ∧ 𝑓(𝑄‘𝑔)𝑝)}))    ⇒   ⊢ (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃)))
Theorem	wksonproplemOLD 29633*	Obsolete version of wksonproplem 29632 as of 13-Dec-2024. (Contributed by AV, 16-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃)))    &   ⊢ 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑂‘𝑔)𝑏)𝑝 ∧ 𝑓(𝑄‘𝑔)𝑝)}))    &   ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑓(𝑄‘𝐺)𝑝) → 𝑓(Walks‘𝐺)𝑝)    ⇒   ⊢ (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃)))
Theorem	trlsonfval 29634*	The set of trails between two vertices. (Contributed by Alexander van der Vekens, 4-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 15-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(TrailsOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(WalksOn‘𝐺)𝐵)𝑝 ∧ 𝑓(Trails‘𝐺)𝑝)})
Theorem	istrlson 29635	Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃)))
Theorem	trlsonprop 29636	Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃)))
Theorem	trlsonistrl 29637	A trail between two vertices is a trail. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 7-Jan-2021.)
⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → 𝐹(Trails‘𝐺)𝑃)
Theorem	trlsonwlkon 29638	A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.)
⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃)
Theorem	trlontrl 29639	A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021.)
⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹((𝑃‘0)(TrailsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃)
17.3.4  Paths and simple paths
Syntax	cpths 29640	Extend class notation with paths (of a graph).
class Paths
Syntax	cspths 29641	Extend class notation with simple paths (of a graph).
class SPaths
Syntax	cpthson 29642	Extend class notation with paths between two vertices (within a graph).
class PathsOn
Syntax	cspthson 29643	Extend class notation with simple paths between two vertices (within a graph).
class SPathsOn
Definition	df-pths 29644*	Define the set of all paths (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." According to Bollobas: "... a path is a walk with distinct vertices.", see Notation of [Bollobas] p. 5. (A walk with distinct vertices is actually a simple path, see upgrwlkdvspth 29669). Therefore, a path can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, which is injective restricted to the set { 1 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ Paths = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝑔)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)})
Definition	df-spths 29645*	Define the set of all simple paths (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." Therefore, a simple path can be represented by an injective mapping f from { 1 , ... , n } and an injective mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the simple path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ SPaths = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝑔)𝑝 ∧ Fun ◡𝑝)})
Definition	df-pthson 29646*	Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ PathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)}))
Definition	df-spthson 29647*	Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.)
⊢ SPathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(SPaths‘𝑔)𝑝)}))
Theorem	relpths 29648	The set (Paths‘𝐺) of all paths on 𝐺 is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021.)
⊢ Rel (Paths‘𝐺)
Theorem	pthsfval 29649*	The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (Paths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)}
Theorem	spthsfval 29650*	The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (SPaths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡𝑝)}
Theorem	ispth 29651	Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅))
Theorem	isspth 29652	Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃))
Theorem	pthistrl 29653	A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃)
Theorem	spthispth 29654	A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃)
Theorem	pthiswlk 29655	A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	spthiswlk 29656	A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	pthdivtx 29657	The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝐼 ∈ (1..^(♯‘𝐹)) ∧ 𝐽 ∈ (0...(♯‘𝐹)) ∧ 𝐼 ≠ 𝐽)) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))
Theorem	pthdadjvtx 29658	The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 𝐼 ∈ (0..^(♯‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘(𝐼 + 1)))
Theorem	dfpth2 29659	Alternate definition for a pair of classes/functions to be a path (in an undirected graph). (Contributed by AV, 4-Oct-2025.)
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))))
Theorem	pthdifv 29660	The vertices of a path are distinct (except the first and last vertex), so the restricted vertex function is one-to-one. (Contributed by AV, 2-Oct-2025.)
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺))
Theorem	2pthnloop 29661*	A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon 30080. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))2 ≤ (♯‘(𝐼‘(𝐹‘𝑖))))
Theorem	upgr2pthnlp 29662*	A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))(♯‘(𝐼‘(𝐹‘𝑖))) = 2)
Theorem	spthdifv 29663	The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))–1-1→(Vtx‘𝐺))
Theorem	spthdep 29664	A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ ((𝐹(SPaths‘𝐺)𝑃 ∧ (♯‘𝐹) ≠ 0) → (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))
Theorem	pthdepisspth 29665	A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 12-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	upgrwlkdvdelem 29666*	Lemma for upgrwlkdvde 29667. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.)
⊢ ((𝑃:(0...(♯‘𝐹))–1-1→𝑉 ∧ 𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹))
Theorem	upgrwlkdvde 29667	In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 29668. (Contributed by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → Fun ◡𝐹)
Theorem	upgrspthswlk 29668*	The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p0, p1, p2 } be a hyperedge, then ( p0, e, p1, e, p2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021.) (Proof shortened by AV, 17-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐺 ∈ UPGraph → (SPaths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ◡𝑝)})
Theorem	upgrwlkdvspth 29669	A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 29668. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	pthsonfval 29670*	The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(PathsOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(Paths‘𝐺)𝑝)})
Theorem	spthson 29671*	The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(SPathsOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(SPaths‘𝐺)𝑝)})
Theorem	ispthson 29672	Properties of a pair of functions to be a path between two given vertices. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃)))
Theorem	isspthson 29673	Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃)))
Theorem	pthsonprop 29674	Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃)))
Theorem	spthonprop 29675	Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃)))
Theorem	pthonispth 29676	A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 17-Jan-2021.)
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(Paths‘𝐺)𝑃)
Theorem	pthontrlon 29677	A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.)
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃)
Theorem	pthonpth 29678	A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃)
Theorem	isspthonpth 29679	A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)))
Theorem	spthonisspth 29680	A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 18-Jan-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(SPaths‘𝐺)𝑃)
Theorem	spthonpthon 29681	A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃)
Theorem	spthonepeq 29682	The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 18-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (♯‘𝐹) = 0))
Theorem	uhgrwkspthlem1 29683	Lemma 1 for uhgrwkspth 29685. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → Fun ◡𝐹)
Theorem	uhgrwkspthlem2 29684	Lemma 2 for uhgrwkspth 29685. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ ((♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) → Fun ◡𝑃)
Theorem	uhgrwkspth 29685	Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) (Revised by AV, 7-Jul-2022.)
⊢ ((𝐺 ∈ 𝑊 ∧ (♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃))
Theorem	usgr2wlkneq 29686	The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
⊢ (((𝐺 ∈ USGraph ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))
Theorem	usgr2wlkspthlem1 29687	Lemma 1 for usgr2wlkspth 29689. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝐹)
Theorem	usgr2wlkspthlem2 29688	Lemma 2 for usgr2wlkspth 29689. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝑃)
Theorem	usgr2wlkspth 29689	In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃))
Theorem	usgr2trlncl 29690	In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2)))
Theorem	usgr2trlspth 29691	In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃))
Theorem	usgr2pthspth 29692	In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Paths‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃))
Theorem	usgr2pthlem 29693*	Lemma for usgr2pth 29694. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))
Theorem	usgr2pth 29694*	In a simple graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))
Theorem	usgr2pth0 29695*	In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑧 ∧ (𝑃‘2) = 𝑦) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑧} ∧ (𝐼‘(𝐹‘1)) = {𝑧, 𝑦})))))
Theorem	pthdlem1 29696*	Lemma 1 for pthd 29699. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ (𝜑 → Fun ◡(𝑃 ↾ (1..^𝑅)))
Theorem	pthdlem2lem 29697*	Lemma for pthdlem2 29698. (Contributed by AV, 10-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅)))
Theorem	pthdlem2 29698*	Lemma 2 for pthd 29699. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅)
Theorem	pthd 29699*	Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    &   ⊢ (♯‘𝐹) = 𝑅    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)
17.3.5  Closed walks
Syntax	cclwlks 29700	Extend class notation with closed walks (of a graph).
class ClWalks