P. 169 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16801-16900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wksfval 16801*	The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. W -> (Walks ` G ) = { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... (♯ ` f ) ) --> V /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) } )
Theorem	iswlk 16802*	Properties of a pair of functions to be/represent a walk. (Contributed by AV, 30-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F (Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) )if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
Theorem	wlkpropg 16803*	Properties of a walk. (Contributed by AV, 5-Nov-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) )if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
Theorem	wlkex 16804	The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
|- ( G e. V -> (Walks ` G ) e. _V )
Theorem	wlkv 16805	The classes involved in a walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.)
|- ( F (Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
Theorem	wlkprop 16806*	Properties of a walk. (Contributed by AV, 5-Nov-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( F (Walks ` G ) P -> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) )if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
Theorem	wlkvg 16807	The classes involved in a walk are sets. Now that we have wlkv 16805 there is no reason to use this theorem in new proofs and using wlkv 16805 is encouraged for consistency with the Metamath Proof Explorer. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.) (New usage is discouraged.)
|- ( ( G e. W /\ F (Walks ` G ) P ) -> ( F e. _V /\ P e. _V ) )
Theorem	iswlkg 16808*	Generalization of iswlk 16802: Conditions for two classes to represent a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. W -> ( F (Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) )if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
Theorem	wlkf 16809	The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( F (Walks ` G ) P -> F e. Word dom I )
Theorem	wlkfg 16810	The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> F e. Word dom I )
Theorem	wlkcl 16811	A walk has length ♯ ( F ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- ( F (Walks ` G ) P -> (♯ ` F ) e. NN0 )
Theorem	wlkclg 16812	A walk has length ♯ ( F ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- ( ( G e. W /\ F (Walks ` G ) P ) -> (♯ ` F ) e. NN0 )
Theorem	wlkp 16813	The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> P : ( 0 ... (♯ ` F ) ) --> V )
Theorem	wlkpg 16814	The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> P : ( 0 ... (♯ ` F ) ) --> V )
Theorem	wlkpwrdg 16815	The sequence of vertices of a walk is a word over the set of vertices. (Contributed by AV, 27-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> P e. Word V )
Theorem	wlklenvp1 16816	The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.)
|- ( F (Walks ` G ) P -> (♯ ` P ) = ( (♯ ` F ) + 1 ) )
Theorem	wlklenvp1g 16817	The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.)
|- ( ( G e. W /\ F (Walks ` G ) P ) -> (♯ ` P ) = ( (♯ ` F ) + 1 ) )
Theorem	wlkm 16818*	The sequence of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- ( F (Walks ` G ) P -> E. x x e. P )
Theorem	wlkvtxm 16819*	A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> E. x x e. V )
Theorem	wlklenvm1 16820	The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- ( F (Walks ` G ) P -> (♯ ` F ) = ( (♯ ` P ) - 1 ) )
Theorem	wlklenvm1g 16821	The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- ( ( G e. W /\ F (Walks ` G ) P ) -> (♯ ` F ) = ( (♯ ` P ) - 1 ) )
Theorem	ifpsnprss 16822	Lemma for wlkvtxeledgg 16823: Two adjacent (not necessarily different) vertices A and B in a walk are incident with an edge E. (Contributed by AV, 4-Apr-2021.) (Revised by AV, 5-Nov-2021.)
|- (if- ( A = B , E = { A } , { A , B } C_ E ) -> { A , B } C_ E )
Theorem	wlkvtxeledgg 16823*	Each pair of adjacent vertices in a walk is a subset of an edge. (Contributed by AV, 28-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
Theorem	wlkvtxiedg 16824*	The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( F (Walks ` G ) P -> A. k e. ( 0..^ (♯ ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
Theorem	wlkvtxiedgg 16825*	The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
Theorem	relwlk 16826	The set (Walks ` G ) of all walks on G is a set of pairs by our definition of a walk, and so is a relation. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 19-Feb-2021.)
|- Rel (Walks ` G )
Theorem	wlkop 16827	A walk is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 1-Jan-2021.)
|- ( W e. (Walks ` G ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
Theorem	wlkelvv 16828	A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
|- ( W e. (Walks ` G ) -> W e. ( _V X. _V ) )
Theorem	wlkcprim 16829	A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Revised by Jim Kingdon, 1-Feb-2026.)
|- ( W e. (Walks ` G ) -> ( 1st ` W ) (Walks ` G ) ( 2nd ` W ) )
Theorem	wlk2f 16830*	If there is a walk W there is a pair of functions representing this walk. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- ( W e. (Walks ` G ) -> E. f E. p f (Walks ` G ) p )
Theorem	wlkcompim 16831*	Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = ( 1st ` W )   &    |- P = ( 2nd ` W )   =>    |- ( W e. (Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) )if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
Theorem	wlkelwrd 16832	The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = ( 1st ` W )   &    |- P = ( 2nd ` W )   =>    |- ( W e. (Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V ) )
Theorem	wlkeq 16833*	Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.) (Revised by AV, 14-Apr-2021.)
|- ( ( A e. (Walks ` G ) /\ B e. (Walks ` G ) /\ N = (♯ ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = (♯ ` ( 1st ` B ) ) /\ A. x e. ( 0..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
Theorem	edginwlkd 16834	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 9-Dec-2021.) (Revised by Jim Kingdon, 2-Feb-2026.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> F e. Word dom I )   &    |- ( ph -> K e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( I ` ( F ` K ) ) e. E )
Theorem	upgredginwlk 16835	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ F e. Word dom I ) -> ( K e. ( 0..^ (♯ ` F ) ) -> ( I ` ( F ` K ) ) e. E ) )
Theorem	iedginwlk 16836	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 23-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( ( Fun I /\ F (Walks ` G ) P /\ X e. ( 0..^ (♯ ` F ) ) ) -> ( I ` ( F ` X ) ) e. ran I )
Theorem	wlkl1loop 16837	A walk of length 1 from a vertex to itself is a loop. (Contributed by AV, 23-Apr-2021.)
|- ( ( ( Fun (iEdg ` G ) /\ F (Walks ` G ) P ) /\ ( (♯ ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. (Edg ` G ) )
Theorem	wlk1walkdom 16838*	A walk is a 1-walk "on the edge level" according to Aksoy et al. (Contributed by AV, 30-Dec-2020.)
|- I = (iEdg ` G )   =>    |- ( F (Walks ` G ) P -> A. k e. ( 1..^ (♯ ` F ) ) 1o ~<_ ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) )
Theorem	upgriswlkdc 16839*	Properties of a pair of functions to be a walk in a pseudograph. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 28-Oct-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. UPGraph -> ( F (Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) ) (DECID ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) ) )
Theorem	upgrwlkedg 16840*	The edges of a walk in a pseudograph join exactly the two corresponding adjacent vertices in the walk. (Contributed by AV, 27-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
Theorem	upgrwlkcompim 16841*	Implications for the properties of the components of a walk in a pseudograph. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 14-Apr-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = ( 1st ` W )   &    |- P = ( 2nd ` W )   =>    |- ( ( G e. UPGraph /\ W e. (Walks ` G ) ) -> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
Theorem	wlkvtxedg 16842*	The vertices of a walk are connected by edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- E = (Edg ` G )   =>    |- ( F (Walks ` G ) P -> A. k e. ( 0..^ (♯ ` F ) ) E. e e. E { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
Theorem	upgrwlkvtxedg 16843*	The pairs of connected vertices of a walk are edges in a pseudograph. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E )
Theorem	uspgr2wlkeq 16844*	Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.) (Revised by AV, 14-Apr-2021.)
|- ( ( G e. USPGraph /\ ( A e. (Walks ` G ) /\ B e. (Walks ` G ) ) /\ N = (♯ ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = (♯ ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) ) )
Theorem	uspgr2wlkeq2 16845	Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.)
|- ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. (Walks ` G ) /\ (♯ ` ( 1st ` A ) ) = N ) /\ ( B e. (Walks ` G ) /\ (♯ ` ( 1st ` B ) ) = N ) ) -> ( ( 2nd ` A ) = ( 2nd ` B ) -> A = B ) )
Theorem	uspgr2wlkeqi 16846	Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 6-May-2021.)
|- ( ( G e. USPGraph /\ ( A e. (Walks ` G ) /\ B e. (Walks ` G ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> A = B )
Theorem	umgrwlknloop 16847*	In a multigraph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 3-Jan-2021.)
|- ( ( G e. UMGraph /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
Theorem	wlkv0 16848	If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- ( ( (Vtx ` G ) = (/) /\ W e. (Walks ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) )
Theorem	g0wlk0 16849	There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- ( (Vtx ` G ) = (/) -> (Walks ` G ) = (/) )
Theorem	0wlk0 16850	There is no walk for the empty set, i.e. in a null graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- (Walks ` (/) ) = (/)
Theorem	wlk0prc 16851	There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- ( ( S e/ _V /\ (Vtx ` S ) = (Vtx ` G ) ) -> (Walks ` G ) = (/) )
Theorem	wlklenvclwlk 16852	The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 2-May-2021.) (Revised by JJ, 14-Jan-2024.)
|- ( W e. Word (Vtx ` G ) -> ( <. F , ( W ++ <" ( W ` 0 ) "> ) >. e. (Walks ` G ) -> (♯ ` F ) = (♯ ` W ) ) )
Theorem	wlkpvtx 16853	A walk connects vertices. (Contributed by AV, 22-Feb-2021.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> ( N e. ( 0 ... (♯ ` F ) ) -> ( P ` N ) e. V ) )
Theorem	wlkepvtx 16854	The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> ( ( P ` 0 ) e. V /\ ( P ` (♯ ` F ) ) e. V ) )
Theorem	2wlklem 16855*	Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
|- ( A. k e. { 0 , 1 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( E ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
Theorem	upgr2wlkdc 16856*	Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 28-Oct-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. UPGraph -> ( ( F (Walks ` G ) P /\ F ~~ 2o ) <-> ( ( F : ( 0..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ A. k e. { 0 , 1 }DECID ( P ` k ) = ( P ` ( k + 1 ) ) ) /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
Theorem	wlkreslem 16857	Lemma for wlkres 16858. (Contributed by AV, 5-Mar-2021.) (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Walks ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> (Vtx ` S ) = V )   =>    |- ( ph -> S e. _V )
Theorem	wlkres 16858	The restriction <. H , Q >. of a walk <. F , P >. to an initial segment of the walk (of length N) forms a walk on the subgraph S consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Walks ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- H = ( F prefix N )   &    |- Q = ( P |` ( 0 ... N ) )   =>    |- ( ph -> H (Walks ` S ) Q )
12.3.2  Trails
Syntax	ctrls 16859	Extend class notation with trails (within a graph).
class Trails
Definition	df-trls 16860*	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 = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
Theorem	reltrls 16861	The set (Trails ` G ) of all trails on G is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021.)
|- Rel (Trails ` G )
Theorem	trlsfvalg 16862*	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.)
|- ( G e. V -> (Trails ` G ) = { <. f , p >. | ( f (Walks ` G ) p /\ Fun `' f ) } )
Theorem	trlsv 16863	The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
|- ( F (Trails ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
Theorem	istrl 16864	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.)
|- ( F (Trails ` G ) P <-> ( F (Walks ` G ) P /\ Fun `' F ) )
Theorem	trliswlk 16865	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.)
|- ( F (Trails ` G ) P -> F (Walks ` G ) P )
Theorem	trlsex 16866	The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.)
|- ( G e. V -> (Trails ` G ) e. _V )
Theorem	trlf1 16867	The enumeration F of a trail <. F , P >. is injective. (Contributed by AV, 20-Feb-2021.) (Proof shortened by AV, 29-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (Trails ` G ) P -> F : ( 0..^ (♯ ` F ) ) -1-1-> dom I )
Theorem	trlreslem 16868	Lemma for trlres 16869. (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.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- H = ( F prefix N )   =>    |- ( ph -> H : ( 0..^ (♯ ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0..^ N ) ) ) )
Theorem	trlres 16869	The restriction <. H , Q >. of a trail <. F , P >. to an initial segment of the trail (of length N) forms a trail on the subgraph S 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.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- H = ( F prefix N )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- Q = ( P |` ( 0 ... N ) )   =>    |- ( ph -> H (Trails ` S ) Q )
12.3.3  Closed walks as words
12.3.3.1  Closed walks as words
Syntax	cclwwlk 16870	Extend class notation with closed walks (in an undirected graph) as word over the set of vertices.
class ClWWalks
Definition	df-clwwlk 16871*	Define the set of all closed walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined elsewhere. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- ClWWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )
Theorem	clwwlkg 16872*	The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. W -> (ClWWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { (lastS ` w ) , ( w ` 0 ) } e. E ) } )
Theorem	isclwwlk 16873*	Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. (ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) )
Theorem	clwwlkbp 16874	Basic properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. (ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) )
Theorem	clwwlkgt0 16875	There is no empty closed walk (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( W e. (ClWWalks ` G ) -> 0 < (♯ ` W ) )
Theorem	clwwlksswrd 16876	Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.)
|- (ClWWalks ` G ) C_ Word (Vtx ` G )
Theorem	clwwlkex 16877	Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
|- ( G e. V -> (ClWWalks ` G ) e. _V )
Theorem	clwwlk1loop 16878	A closed walk of length 1 is a loop. (Contributed by AV, 24-Apr-2021.)
|- ( ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = 1 ) -> { ( W ` 0 ) , ( W ` 0 ) } e. (Edg ` G ) )
Theorem	clwwlkccatlem 16879*	Lemma for clwwlkccat 16880: index j is shifted up by (♯ ` A ), and the case i = ( (♯ ` A ) - 1 ) is covered by the "bridge" { (lastS ` A ) , ( B ` 0 ) } = { (lastS ` A ) , ( A ` 0 ) } e. (Edg ` G ). (Contributed by AV, 23-Apr-2022.)
|- ( ( ( ( A e. Word (Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0..^ ( (♯ ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. (Edg ` G ) /\ { (lastS ` A ) , ( A ` 0 ) } e. (Edg ` G ) ) /\ ( ( B e. Word (Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0..^ ( (♯ ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. (Edg ` G ) /\ { (lastS ` B ) , ( B ` 0 ) } e. (Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( 0..^ ( (♯ ` ( A ++ B ) ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. (Edg ` G ) )
Theorem	clwwlkccat 16880	The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 23-Apr-2022.)
|- ( ( A e. (ClWWalks ` G ) /\ B e. (ClWWalks ` G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. (ClWWalks ` G ) )
Theorem	umgrclwwlkge2 16881	A closed walk in a multigraph has a length of at least 2 (because it cannot have a loop). (Contributed by Alexander van der Vekens, 16-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( G e. UMGraph -> ( P e. (ClWWalks ` G ) -> 2 <_ (♯ ` P ) ) )
12.3.3.2  Closed walks of a fixed length as words
Syntax	cclwwlkn 16882	Extend class notation with closed walks (in an undirected graph) of a fixed length as word over the set of vertices.
class ClWWalksN
Definition	df-clwwlkn 16883*	Define the set of all closed walks of a fixed length n as words over the set of vertices in a graph g. If 0 < n, such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) . For n = 0, the set is empty, see clwwlkn0 16887. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
Theorem	clwwlkng 16884*	The set of closed walks of a fixed length N as words over the set of vertices in a graph G. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( ( N e. NN0 /\ G e. V ) -> ( N ClWWalksN G ) = { w e. (ClWWalks ` G ) | (♯ ` w ) = N } )
Theorem	isclwwlkng 16885	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( N e. NN0 -> ( W e. ( N ClWWalksN G ) <-> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) ) )
Theorem	isclwwlkni 16886	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Jim Kingdon, 22-Feb-2026.)
|- ( W e. ( N ClWWalksN G ) -> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) )
Theorem	clwwlkn0 16887	There is no closed walk of length 0 (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( 0 ClWWalksN G ) = (/)
Theorem	clwwlkclwwlkn 16888	A closed walk of a fixed length as word is a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> W e. (ClWWalks ` G ) )
Theorem	clwwlksclwwlkn 16889	The closed walks of a fixed length as words are closed walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 12-Apr-2021.)
|- ( N ClWWalksN G ) C_ (ClWWalks ` G )
Theorem	clwwlknlen 16890	The length of a word representing a closed walk of a fixed length is this fixed length. (Contributed by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> (♯ ` W ) = N )
Theorem	clwwlknnn 16891	The length of a closed walk of a fixed length as word is a positive integer. (Contributed by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> N e. NN )
Theorem	isclwwlkn 16892	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) <-> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) )
Theorem	clwwlknwrd 16893	A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> W e. Word V )
Theorem	clwwlknbp 16894	Basic properties of a closed walk of a fixed length as word. (Contributed by AV, 30-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- V = (Vtx ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> ( W e. Word V /\ (♯ ` W ) = N ) )
Theorem	isclwwlknx 16895*	Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( N e. NN -> ( W e. ( N ClWWalksN G ) <-> ( ( W e. Word V /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) /\ (♯ ` W ) = N ) ) )
Theorem	clwwlknp 16896*	Properties of a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 23-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> ( ( W e. Word V /\ (♯ ` W ) = N ) /\ A. i e. ( 0..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) )
Theorem	clwwlkn1 16897	A closed walk of length 1 represented as word is a word consisting of 1 symbol representing a vertex connected to itself by (at least) one edge, that is, a loop. (Contributed by AV, 24-Apr-2021.) (Revised by AV, 11-Feb-2022.)
|- ( W e. ( 1 ClWWalksN G ) <-> ( (♯ ` W ) = 1 /\ W e. Word (Vtx ` G ) /\ { ( W ` 0 ) } e. (Edg ` G ) ) )
Theorem	loopclwwlkn1b 16898	The singleton word consisting of a vertex V represents a closed walk of length 1 iff there is a loop at vertex V. (Contributed by AV, 11-Feb-2022.)
|- ( V e. (Vtx ` G ) -> ( { V } e. (Edg ` G ) <-> <" V "> e. ( 1 ClWWalksN G ) ) )
Theorem	clwwlkn1loopb 16899*	A word represents a closed walk of length 1 iff this word is a singleton word consisting of a vertex with an attached loop. (Contributed by AV, 11-Feb-2022.)
|- ( W e. ( 1 ClWWalksN G ) <-> E. v e. (Vtx ` G ) ( W = <" v "> /\ { v } e. (Edg ` G ) ) )
Theorem	clwwlkn2 16900	A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Apr-2021.)
|- ( W e. ( 2 ClWWalksN G ) <-> ( (♯ ` W ) = 2 /\ W e. Word (Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. (Edg ` G ) ) )