P. 262 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26101-26200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0spth 26101	A pair of an empty set (of edges) and a second set (of vertices) is a simple path if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑃 ∈ 𝑍) → (∅(𝑉 SPaths 𝐸)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	pthistrl 26102	A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.)
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → 𝐹(𝑉 Trails 𝐸)𝑃)
Theorem	spthispth 26103	A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.)
⊢ (𝐹(𝑉 SPaths 𝐸)𝑃 → 𝐹(𝑉 Paths 𝐸)𝑃)
Theorem	pthdepisspth 26104	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.)
⊢ ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → 𝐹(𝑉 SPaths 𝐸)𝑃)
Theorem	pthon 26105*	The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 PathOn 𝐸)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Paths 𝐸)𝑝)})
Theorem	ispthon 26106	Properties of a pair of functions to be a path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 PathOn 𝐸)𝐵)𝑃 ↔ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 Paths 𝐸)𝑃)))
Theorem	pthonprop 26107	Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.)
⊢ (𝐹(𝐴(𝑉 PathOn 𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 Paths 𝐸)𝑃)))
Theorem	pthonispth 26108	A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.)
⊢ (𝐹(𝐴(𝑉 PathOn 𝐸)𝐵)𝑃 → 𝐹(𝑉 Paths 𝐸)𝑃)
Theorem	0pthon 26109	A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑁 ∈ 𝑉) → ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(𝑉 PathOn 𝐸)𝑁)𝑃))
Theorem	0pthon1 26110	A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑁 ∈ 𝑉) → ∅(𝑁(𝑉 PathOn 𝐸)𝑁){⟨0, 𝑁⟩})
Theorem	0pthonv 26111*	For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑁 ∈ 𝑉 → ∃𝑓∃𝑝 𝑓(𝑁(𝑉 PathOn 𝐸)𝑁)𝑝))
Theorem	spthon 26112*	The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 SPathOn 𝐸)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝)})
Theorem	isspthon 26113	Properties of a pair of functions to be a simple path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 ↔ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃)))
Theorem	isspthonpth 26114	Properties of a pair of functions to be a simple path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 9-Mar-2018.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 ↔ (𝐹(𝑉 SPaths 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)))
Theorem	spthonprp 26115	Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
⊢ (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃)))
Theorem	spthonisspth 26116	A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
⊢ (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 → 𝐹(𝑉 SPaths 𝐸)𝑃)
Theorem	spthonepeq 26117	The endpoints of a simple path between two vertices are equal if and only if the path is of length 0 (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
⊢ (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))
Theorem	constr1trl 26118	Construction of a trail from one given edge in a graph. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ 𝐹 = {⟨0, 𝑖⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩}    ⇒   ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 𝐹(𝑉 Trails 𝐸)𝑃)
Theorem	1pthonlem1 26119	Lemma 1 for 1pthon 26121. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ 𝐹 = {⟨0, 𝑖⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩}    ⇒   ⊢ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))
Theorem	1pthonlem2 26120	Lemma 2 for 1pthon 26121. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ 𝐹 = {⟨0, 𝑖⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩}    ⇒   ⊢ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅
Theorem	1pthon 26121	A path of length 1 from one vertex to another vertex. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → {⟨0, 𝑖⟩} (𝐴(𝑉 PathOn 𝐸)𝐵){⟨0, 𝐴⟩, ⟨1, 𝐵⟩})
Theorem	1pthoncl 26122	A path of length 1 from one vertex to another vertex. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐼 ∈ V ∧ (𝐸‘𝐼) = {𝐴, 𝐵})) → {⟨0, 𝐼⟩} (𝐴(𝑉 PathOn 𝐸)𝐵){⟨0, 𝐴⟩, ⟨1, 𝐵⟩})
Theorem	1pthon2v 26123*	For each pair of adjacent vertices there is a path of length 1 from one vertex to the other. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵}) → ∃𝑓∃𝑝 𝑓(𝐴(𝑉 PathOn 𝐸)𝐵)𝑝)
Theorem	constr2spthlem1 26124	Lemma 1 for constr2spth 26130. (Contributed by Alexander van der Vekens, 31-Jan-2018.)
⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ◡𝑃)
Theorem	2pthlem1 26125	Lemma 1 for constr2pth 26131. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by Alexander van der Vekens, 31-Jan-2018.)
⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → Fun ◡(𝑃 ↾ (1..^2)))
Theorem	2pthlem2 26126	Lemma 2 for constr2pth 26131. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by Alexander van der Vekens, 18-Feb-2018.)
⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ((𝑃 “ {0, 2}) ∩ (𝑃 “ (1..^2))) = ∅)
Theorem	2wlklem1 26127*	Lemma 1 for constr2wlk 26128. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊)    &   ⊢ 𝐹 = {⟨0, 𝐼⟩, ⟨1, 𝐽⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → ∀𝑘 ∈ {0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})
Theorem	constr2wlk 26128	Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018.)
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊)    &   ⊢ 𝐹 = {⟨0, 𝐼⟩, ⟨1, 𝐽⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → 𝐹(𝑉 Walks 𝐸)𝑃))
Theorem	constr2trl 26129	Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by Alexander van der Vekens, 1-Feb-2018.)
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊)    &   ⊢ 𝐹 = {⟨0, 𝐼⟩, ⟨1, 𝐽⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → 𝐹(𝑉 Trails 𝐸)𝑃))
Theorem	constr2spth 26130	A simple path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊)    &   ⊢ 𝐹 = {⟨0, 𝐼⟩, ⟨1, 𝐽⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → 𝐹(𝑉 SPaths 𝐸)𝑃))
Theorem	constr2pth 26131	A path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by Alexander van der Vekens, 31-Jan-2018.)
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊)    &   ⊢ 𝐹 = {⟨0, 𝐼⟩, ⟨1, 𝐽⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → 𝐹(𝑉 Paths 𝐸)𝑃))
Theorem	2pthon 26132	A path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶}) → {⟨0, 𝑖⟩, ⟨1, 𝑗⟩} (𝐴(𝑉 PathOn 𝐸)𝐶){⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}))
Theorem	2pthoncl 26133	A path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝐼 ∈ V ∧ 𝐽 ∈ V) ∧ (𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → {⟨0, 𝐼⟩, ⟨1, 𝐽⟩} (𝐴(𝑉 PathOn 𝐸)𝐶){⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩})
Theorem	2pthon3v 26134*	For a vertex adjacent to two other vertices there is a path of length 2 between these other vertices. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ((◡𝐸‘{𝐴, 𝐵}) ≠ (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) → ∃𝑓∃𝑝(𝑓(𝐴(𝑉 PathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2))
Theorem	redwlklem 26135	Lemma for redwlk 26136. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))) = ((#‘𝐹) − 1))
Theorem	redwlk 26136	A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(𝑉 Walks 𝐸)(𝑃 ↾ (0..^(#‘𝐹))))
Theorem	wlkdvspthlem 26137*	Lemma for wlkdvspth 26138. (Contributed by Alexander van der Vekens, 27-Oct-2017.)
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → Fun ◡𝐹)
Theorem	wlkdvspth 26138	A walk consisting of different vertices is a simple path. (Contributed by Alexander van der Vekens, 27-Oct-2017.)
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ Fun ◡𝑃) → 𝐹(𝑉 SPaths 𝐸)𝑃)
Theorem	usgra2adedgspthlem1 26139	Lemma 1 for usgra2adedgspth 26141. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶}))
Theorem	usgra2adedgspthlem2 26140	Lemma 2 for usgra2adedgspth 26141. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ (((𝑉 USGrph 𝐸 ∧ 𝐴 ≠ 𝐶) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((◡𝐸‘{𝐴, 𝐵}) ≠ (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶}))
Theorem	usgra2adedgspth 26141	In an undirected simple graph, two adjacent edges form a simple path of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝐴 ≠ 𝐶) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → 𝐹(𝑉 SPaths 𝐸)𝑃))
Theorem	usgra2adedgwlk 26142	In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)))))
Theorem	usgra2adedgwlkon 26143	In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃))
Theorem	usgra2adedgwlkonALT 26144	Alternate proof for usgra2adedgwlkon 26143, using usgra2adedgwlk 26142, but with a longer proof! In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩}    &   ⊢ 𝑃 = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩}    ⇒   ⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑃))
Theorem	usg2wlk 26145*	In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))
Theorem	usg2wlkon 26146*	In an undirected simple graph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ∃𝑓∃𝑝 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝))
Theorem	usgra2wlkspthlem1 26147*	Lemma 1 for usgra2wlkspth 26149. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸 ∧ (#‘𝐹) = 2) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝐹))
Theorem	usgra2wlkspthlem2 26148*	Lemma 2 for usgra2wlkspth 26149. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ (𝑉 USGrph 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝑃))
Theorem	usgra2wlkspth 26149	In a undirected simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ↔ 𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃))
17.1.5.3  Circuits and cycles
Theorem	crcts 26150*	The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 Circuits 𝐸) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))})
Theorem	cycls 26151*	The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 Cycles 𝐸) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑉 Paths 𝐸)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))})
Theorem	iscrct 26152	Properties of a pair of functions to be a circuit (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Circuits 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))
Theorem	iscycl 26153	Properties of a pair of functions to be a cycle (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))
Theorem	0crct 26154	A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑃 ∈ 𝑍) → (∅(𝑉 Circuits 𝐸)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	0cycl 26155	A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑃 ∈ 𝑍) → (∅(𝑉 Cycles 𝐸)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	crctistrl 26156	A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (𝐹(𝑉 Circuits 𝐸)𝑃 → 𝐹(𝑉 Trails 𝐸)𝑃)
Theorem	cyclispth 26157	A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Paths 𝐸)𝑃)
Theorem	cycliscrct 26158	A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Circuits 𝐸)𝑃)
Theorem	cyclnspth 26159	A (non trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (𝐹 ≠ ∅ → (𝐹(𝑉 Cycles 𝐸)𝑃 → ¬ 𝐹(𝑉 SPaths 𝐸)𝑃))
Theorem	cycliswlk 26160	A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.)
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃)
Theorem	cyclispthon 26161	A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.)
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹((𝑃‘0)(𝑉 PathOn 𝐸)(𝑃‘0))𝑃)
Theorem	fargshiftlem 26162	If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ (0..^𝑁)) → (𝑋 + 1) ∈ (1...𝑁))
Theorem	fargshiftfv 26163*	If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (𝑋 ∈ (0..^𝑁) → (𝐺‘𝑋) = (𝐹‘(𝑋 + 1))))
Theorem	fargshiftf 26164*	If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → 𝐺:(0..^(#‘𝐹))⟶dom 𝐸)
Theorem	fargshiftf1 26165*	If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–1-1→dom 𝐸) → 𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸)
Theorem	fargshiftfo 26166*	If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–onto→dom 𝐸) → 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸)
Theorem	fargshiftfva 26167*	The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (∀𝑘 ∈ (1...𝑁)(𝐸‘(𝐹‘𝑘)) = ⦋𝑘 / 𝑥⦌𝑃 → ∀𝑙 ∈ (0..^𝑁)(𝐸‘(𝐺‘𝑙)) = ⦋(𝑙 + 1) / 𝑥⦌𝑃))
Theorem	usgrcyclnl1 26168	In an undirected simple graph (with no loops!) there are no cycles with length 1 (consisting of one edge ). (Contributed by Alexander van der Vekens, 7-Nov-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃) → (#‘𝐹) ≠ 1)
Theorem	usgrcyclnl2 26169	In an undirected simple graph (with no loops!) there are no cycles with length 2 (consisting of two edges ). (Contributed by Alexander van der Vekens, 9-Nov-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃) → (#‘𝐹) ≠ 2)
Theorem	3cycl3dv 26170	In a simple graph, the vertices of a 3-cycle are mutually different. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴))
Theorem	nvnencycllem 26171	Lemma for 3v3e3cycl1 26172 and 4cycl4v4e 26194. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → ((𝐸‘(𝐹‘𝑋)) = {𝐴, 𝐵} → {𝐴, 𝐵} ∈ ran 𝐸))
Theorem	3v3e3cycl1 26172*	If there is a cycle of length 3 in a graph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
⊢ ((Fun 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃 ∧ (#‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))
Theorem	constr3lem1 26173	Lemma for constr3trl 26187 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ (𝐹 ∈ V ∧ 𝑃 ∈ V)
Theorem	constr3lem2 26174	Lemma for constr3trl 26187 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ (#‘𝐹) = 3
Theorem	constr3lem4 26175	Lemma for constr3trl 26187 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)))
Theorem	constr3lem5 26176	Lemma for constr3trl 26187 etc. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴}))
Theorem	constr3lem6 26177	Lemma for constr3pthlem3 26185. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({(𝑃‘0), (𝑃‘3)} ∩ {(𝑃‘1), (𝑃‘2)}) = ∅)
Theorem	constr3trllem1 26178	Lemma for constr3trl 26187. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹 ∈ Word dom 𝐸)
Theorem	constr3trllem2 26179	Lemma for constr3trl 26187. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → Fun ◡𝐹)
Theorem	constr3trllem3 26180	Lemma for constr3trl 26187. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃:(0...(#‘𝐹))⟶𝑉)
Theorem	constr3trllem4 26181	Lemma for constr3trl 26187. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃:(0...3)⟶𝑉)
Theorem	constr3trllem5 26182*	Lemma for constr3trl 26187. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})
Theorem	constr3pthlem1 26183	Lemma for constr3pth 26188. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑃 ↾ (1..^(#‘𝐹))) = {⟨1, 𝐵⟩, ⟨2, 𝐶⟩})
Theorem	constr3pthlem2 26184	Lemma for constr3pth 26188. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹))))
Theorem	constr3pthlem3 26185	Lemma for constr3pth 26188. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)
Theorem	constr3cycllem1 26186	Lemma for constr3cycl 26189. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃‘0) = (𝑃‘(#‘𝐹)))
Theorem	constr3trl 26187	Construction of a trail from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹(𝑉 Trails 𝐸)𝑃)
Theorem	constr3pth 26188	Construction of a path from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹(𝑉 Paths 𝐸)𝑃)
Theorem	constr3cycl 26189	Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ∧ (#‘𝐹) = 3))
Theorem	constr3cyclp 26190	Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
⊢ 𝐹 = {⟨0, (◡𝐸‘{𝐴, 𝐵})⟩, ⟨1, (◡𝐸‘{𝐵, 𝐶})⟩, ⟨2, (◡𝐸‘{𝐶, 𝐴})⟩}    &   ⊢ 𝑃 = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐴⟩})    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ∧ (#‘𝐹) = 3 ∧ (𝑃‘0) = 𝐴))
Theorem	constr3cyclpe 26191*	If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∃𝑓∃𝑝(𝑓(𝑉 Cycles 𝐸)𝑝 ∧ (#‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴))
Theorem	3v3e3cycl2 26192*	If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph. (Contributed by Alexander van der Vekens, 14-Nov-2017.)
⊢ (𝑉 USGrph 𝐸 → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸) → ∃𝑓∃𝑝(𝑓(𝑉 Cycles 𝐸)𝑝 ∧ (#‘𝑓) = 3)))
Theorem	3v3e3cycl 26193*	If and only if there is a 3-cycle in a graph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.)
⊢ (𝑉 USGrph 𝐸 → (∃𝑓∃𝑝(𝑓(𝑉 Cycles 𝐸)𝑝 ∧ (#‘𝑓) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))
Theorem	4cycl4v4e 26194*	If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
⊢ ((Fun 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃 ∧ (#‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)))
Theorem	4cycl4dv 26195	In a simple graph, the vertices of a 4-cycle are mutually different. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹 ∧ (#‘𝐹) = 4)) → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)))))
Theorem	4cycl4dv4e 26196*	If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃 ∧ (#‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ ({𝑐, 𝑑} ∈ ran 𝐸 ∧ {𝑑, 𝑎} ∈ ran 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
17.1.5.4  Connected graphs
Syntax	cconngra 26197	Extend class notation with connected graphs.
class ConnGrph
Definition	df-conngra 26198*	Define the class of all connected graphs. A graph (or, more generally, any pair representing a structure consisting of "vertices" and "edges") is called connected if there is a path between every pair of (distinct) vertices. The distinctness of the vertices is not necessary for the definition, because there is always a path (of length 0) from a vertex to itself, see 0pthonv 26111 and dfconngra1 26199. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
⊢ ConnGrph = {⟨𝑣, 𝑒⟩ ∣ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝}
Theorem	dfconngra1 26199*	Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ ConnGrph = {⟨𝑣, 𝑒⟩ ∣ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝}
Theorem	isconngra 26200*	The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ConnGrph 𝐸 ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝))