P. 255 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25401-25500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscycl 25401	Properties of a pair of functions to be a cycle (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( V Cycles E ) P <-> ( F ( V Paths E ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
Theorem	0crct 25402	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.)
|- ( ( ( V e. X /\ E e. Y ) /\ P e. Z ) -> ( (/) ( V Circuits E ) P <-> P : ( 0 ... 0 ) --> V ) )
Theorem	0cycl 25403	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.)
|- ( ( ( V e. X /\ E e. Y ) /\ P e. Z ) -> ( (/) ( V Cycles E ) P <-> P : ( 0 ... 0 ) --> V ) )
Theorem	crctistrl 25404	A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|- ( F ( V Circuits E ) P -> F ( V Trails E ) P )
Theorem	cyclispth 25405	A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|- ( F ( V Cycles E ) P -> F ( V Paths E ) P )
Theorem	cycliscrct 25406	A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|- ( F ( V Cycles E ) P -> F ( V Circuits E ) P )
Theorem	cyclnspth 25407	A (non trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|- ( F =/= (/) -> ( F ( V Cycles E ) P -> -. F ( V SPaths E ) P ) )
Theorem	cycliswlk 25408	A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.)
|- ( F ( V Cycles E ) P -> F ( V Walks E ) P )
Theorem	cyclispthon 25409	A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.)
|- ( F ( V Cycles E ) P -> F ( ( P ` 0 ) ( V PathOn E ) ( P ` 0 ) ) P )
Theorem	fargshiftlem 25410	If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
|- ( ( N e. NN0 /\ X e. ( 0..^ N ) ) -> ( X + 1 ) e. ( 1 ... N ) )
Theorem	fargshiftfv 25411*	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.)
|- G = ( x e. ( 0..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )   =>    |- ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( X e. ( 0..^ N ) -> ( G ` X ) = ( F ` ( X + 1 ) ) ) )
Theorem	fargshiftf 25412*	If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
|- G = ( x e. ( 0..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )   =>    |- ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> G : ( 0..^ ( # ` F ) ) --> dom E )
Theorem	fargshiftf1 25413*	If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
|- G = ( x e. ( 0..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )   =>    |- ( ( N e. NN0 /\ F : ( 1 ... N ) -1-1-> dom E ) -> G : ( 0..^ ( # ` F ) ) -1-1-> dom E )
Theorem	fargshiftfo 25414*	If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
|- G = ( x e. ( 0..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )   =>    |- ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> G : ( 0..^ ( # ` F ) ) -onto-> dom E )
Theorem	fargshiftfva 25415*	The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
|- G = ( x e. ( 0..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )   =>    |- ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( A. k e. ( 1 ... N ) ( E ` ( F ` k ) ) = [_ k / x ]_ P -> A. l e. ( 0..^ N ) ( E ` ( G ` l ) ) = [_ ( l + 1 ) / x ]_ P ) )
Theorem	usgrcyclnl1 25416	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.)
|- ( ( V USGrph E /\ F ( V Cycles E ) P ) -> ( # ` F ) =/= 1 )
Theorem	usgrcyclnl2 25417	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.)
|- ( ( V USGrph E /\ F ( V Cycles E ) P ) -> ( # ` F ) =/= 2 )
Theorem	3cycl3dv 25418	In a simple graph, the vertices of a 3-cycle are mutually different. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
|- ( ( V USGrph E /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> ( A =/= B /\ B =/= C /\ C =/= A ) )
Theorem	nvnencycllem 25419	Lemma for 3v3e3cycl1 25420 and 4cycl4v4e 25442. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
|- ( ( ( Fun E /\ F e. Word dom E ) /\ ( X e. NN0 /\ X < ( # ` F ) ) ) -> ( ( E ` ( F ` X ) ) = { A , B } -> { A , B } e. ran E ) )
Theorem	3v3e3cycl1 25420*	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 E /\ F ( V Cycles E ) P /\ ( # ` F ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( { a , b } e. ran E /\ { b , c } e. ran E /\ { c , a } e. ran E ) )
Theorem	constr3lem1 25421	Lemma for constr3trl 25435 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( F e. _V /\ P e. _V )
Theorem	constr3lem2 25422	Lemma for constr3trl 25435 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( # ` F ) = 3
Theorem	constr3lem4 25423	Lemma for constr3trl 25435 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = A ) ) )
Theorem	constr3lem5 25424	Lemma for constr3trl 25435 etc. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( F ` 0 ) = ( `' E ` { A , B } ) /\ ( F ` 1 ) = ( `' E ` { B , C } ) /\ ( F ` 2 ) = ( `' E ` { C , A } ) )
Theorem	constr3lem6 25425	Lemma for constr3pthlem3 25433. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( { ( P ` 0 ) , ( P ` 3 ) } i^i { ( P ` 1 ) , ( P ` 2 ) } ) = (/) )
Theorem	constr3trllem1 25426	Lemma for constr3trl 25435. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> F e. Word dom E )
Theorem	constr3trllem2 25427	Lemma for constr3trl 25435. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> Fun `' F )
Theorem	constr3trllem3 25428	Lemma for constr3trl 25435. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( A e. V /\ B e. V /\ C e. V ) -> P : ( 0 ... ( # ` F ) ) --> V )
Theorem	constr3trllem4 25429	Lemma for constr3trl 25435. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( A e. V /\ B e. V /\ C e. V ) -> P : ( 0 ... 3 ) --> V )
Theorem	constr3trllem5 25430*	Lemma for constr3trl 25435. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
Theorem	constr3pthlem1 25431	Lemma for constr3pth 25436. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( B e. V /\ C e. W ) -> ( P |` ( 1..^ ( # ` F ) ) ) = { <. 1 , B >. , <. 2 , C >. } )
Theorem	constr3pthlem2 25432	Lemma for constr3pth 25436. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ B =/= C ) -> Fun `' ( P |` ( 1..^ ( # ` F ) ) ) )
Theorem	constr3pthlem3 25433	Lemma for constr3pth 25436. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ B =/= C /\ C =/= A ) ) -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1..^ ( # ` F ) ) ) ) = (/) )
Theorem	constr3cycllem1 25434	Lemma for constr3cycl 25437. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( A e. V /\ B e. V /\ C e. V ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
Theorem	constr3trl 25435	Construction of a trail from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> F ( V Trails E ) P )
Theorem	constr3pth 25436	Construction of a path from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> F ( V Paths E ) P )
Theorem	constr3cycl 25437	Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> ( F ( V Cycles E ) P /\ ( # ` F ) = 3 ) )
Theorem	constr3cyclp 25438	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.)
|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> ( F ( V Cycles E ) P /\ ( # ` F ) = 3 /\ ( P ` 0 ) = A ) )
Theorem	constr3cyclpe 25439*	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.)
|- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> E. f E. p ( f ( V Cycles E ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )
Theorem	3v3e3cycl2 25440*	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.)
|- ( V USGrph E -> ( E. a e. V E. b e. V E. c e. V ( { a , b } e. ran E /\ { b , c } e. ran E /\ { c , a } e. ran E ) -> E. f E. p ( f ( V Cycles E ) p /\ ( # ` f ) = 3 ) ) )
Theorem	3v3e3cycl 25441*	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.)
|- ( V USGrph E -> ( E. f E. p ( f ( V Cycles E ) p /\ ( # ` f ) = 3 ) <-> E. a e. V E. b e. V E. c e. V ( { a , b } e. ran E /\ { b , c } e. ran E /\ { c , a } e. ran E ) ) )
Theorem	4cycl4v4e 25442*	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 E /\ F ( V Cycles E ) P /\ ( # ` F ) = 4 ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( { a , b } e. ran E /\ { b , c } e. ran E ) /\ ( { c , d } e. ran E /\ { d , a } e. ran E ) ) )
Theorem	4cycl4dv 25443	In a simple graph, the vertices of a 4-cycle are mutually different. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
|- ( ( V USGrph E /\ ( F e. Word dom E /\ Fun `' F /\ ( # ` F ) = 4 ) ) -> ( ( ( ( E ` ( F ` 0 ) ) = { A , B } /\ ( E ` ( F ` 1 ) ) = { B , C } ) /\ ( ( E ` ( F ` 2 ) ) = { C , D } /\ ( E ` ( F ` 3 ) ) = { D , A } ) ) -> ( ( ( { A , B } e. ran E /\ { B , C } e. ran E ) /\ ( { C , D } e. ran E /\ { D , A } e. ran E ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) ) )
Theorem	4cycl4dv4e 25444*	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.)
|- ( ( V USGrph E /\ F ( V Cycles E ) P /\ ( # ` F ) = 4 ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. ran E /\ { b , c } e. ran E ) /\ ( { c , d } e. ran E /\ { d , a } e. ran E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )
16.1.5.4  Connected graphs
Syntax	cconngra 25445	Extend class notation with connected graphs.
class ConnGrph
Definition	df-conngra 25446*	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 25359 and dfconngra1 25447. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
|- ConnGrph = { <. v , e >. | A. k e. v A. n e. v E. f E. p f ( k ( v PathOn e ) n ) p }
Theorem	dfconngra1 25447*	Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
|- ConnGrph = { <. v , e >. | A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( v PathOn e ) n ) p }
Theorem	isconngra 25448*	The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
|- ( ( V e. X /\ E e. Y ) -> ( V ConnGrph E <-> A. k e. V A. n e. V E. f E. p f ( k ( V PathOn E ) n ) p ) )
Theorem	isconngra1 25449*	The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
|- ( ( V e. X /\ E e. Y ) -> ( V ConnGrph E <-> A. k e. V A. n e. ( V \ { k } ) E. f E. p f ( k ( V PathOn E ) n ) p ) )
Theorem	0conngra 25450	A class/graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
|- ( E e. V -> (/) ConnGrph E )
Theorem	1conngra 25451	A class/graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
|- ( E e. V -> { A } ConnGrph E )
Theorem	cusconngra 25452	A complete (undirected simple) graph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
|- ( V ComplUSGrph E -> V ConnGrph E )
16.1.5.5  Walks as words
Syntax	cwwlk 25453	Extend class notation with Walks (of a graph) as Word over the set of vertices.
class WWalks
Syntax	cwwlkn 25454	Extend class notation with Walks (of a graph) of a fixed length as Word over the set of vertices.
class WWalksN
Definition	df-wwlk 25455*	Define the set of all 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) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlk 25284. w = (/) has to be excluded because a walk always consists of at least one vertex, see wlkn0 25303. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- WWalks = ( v e. _V , e e. _V |-> { w e. Word v | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ran e ) } )
Definition	df-wwlkn 25456*	Define the set of all Walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlk 25284. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- WWalksN = ( v e. _V , e e. _V |-> ( n e. NN0 |-> { w e. ( v WWalks e ) | ( # ` w ) = ( n + 1 ) } ) )
Theorem	wwlk 25457*	The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V WWalks E ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ran E ) } )
Theorem	wwlkn 25458*	The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- ( ( V e. X /\ E e. Y /\ N e. NN0 ) -> ( ( V WWalksN E ) ` N ) = { w e. ( V WWalks E ) | ( # ` w ) = ( N + 1 ) } )
Theorem	iswwlk 25459*	Properties of a word to represent a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( W e. ( V WWalks E ) <-> ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ran E ) ) )
Theorem	iswwlkn 25460	Properties of a word to represent a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- ( ( V e. X /\ E e. Y /\ N e. NN0 ) -> ( W e. ( ( V WWalksN E ) ` N ) <-> ( W e. ( V WWalks E ) /\ ( # ` W ) = ( N + 1 ) ) ) )
Theorem	wwlkprop 25461	Properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- ( P e. ( V WWalks E ) -> ( V e. _V /\ E e. _V /\ P e. Word V ) )
Theorem	wwlknprop 25462	Properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018.)
|- ( P e. ( ( V WWalksN E ) ` N ) -> ( ( V e. _V /\ E e. _V ) /\ ( N e. NN0 /\ P e. Word V ) ) )
Theorem	wwlknimp 25463*	Implications for a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.)
|- ( W e. ( ( V WWalksN E ) ` N ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ran E ) )
Theorem	wwlksswrd 25464	Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018.)
|- ( V WWalks E ) C_ Word V
Theorem	wwlkn0 25465*	A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- ( W e. ( ( V WWalksN E ) ` 0 ) -> E. v e. V W = <" v "> )
Theorem	wlkiswwlk1 25466	The sequence of vertices in a walk is a walk as word in an undirected simple graph. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- ( V USGrph E -> ( F ( V Walks E ) P -> P e. ( V WWalks E ) ) )
Theorem	wlkiswwlk2lem1 25467*	Lemma 1 for wlkiswwlk2 25473. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
Theorem	wlkiswwlk2lem2 25468*	Lemma 2 for wlkiswwlk2 25473. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( ( # ` P ) e. NN0 /\ I e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )
Theorem	wlkiswwlk2lem3 25469*	Lemma 3 for wlkiswwlk2 25473. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
Theorem	wlkiswwlk2lem4 25470*	Lemma 4 for wlkiswwlk2 25473. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( V USGrph E /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
Theorem	wlkiswwlk2lem5 25471*	Lemma 5 for wlkiswwlk2 25473. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( V USGrph E /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> F e. Word dom E ) )
Theorem	wlkiswwlk2lem6 25472*	Lemma 6 for wlkiswwlk2 25473. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( V USGrph E /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
Theorem	wlkiswwlk2 25473*	A walk as word corresponds to the sequence of vertices in a walk in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- ( V USGrph E -> ( P e. ( V WWalks E ) -> E. f f ( V Walks E ) P ) )
Theorem	wlkiswwlk 25474*	A walk as word corresponds to a walk in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- ( V USGrph E -> ( E. f f ( V Walks E ) P <-> P e. ( V WWalks E ) ) )
Theorem	wlklniswwlkn1 25475	The sequence of vertices in a walk of length n is a walk as word of length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- ( V USGrph E -> ( ( F ( V Walks E ) P /\ ( # ` F ) = N ) -> P e. ( ( V WWalksN E ) ` N ) ) )
Theorem	wlklniswwlkn2 25476*	A walk of length n as word corresponds to the sequence of vertices in a walk of length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- ( V USGrph E -> ( P e. ( ( V WWalksN E ) ` N ) -> E. f ( f ( V Walks E ) P /\ ( # ` f ) = N ) ) )
Theorem	wlklniswwlkn 25477*	A walk of length n as word corresponds to a walk with length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- ( V USGrph E -> ( E. f ( f ( V Walks E ) P /\ ( # ` f ) = N ) <-> P e. ( ( V WWalksN E ) ` N ) ) )
Theorem	wwlkiswwlkn 25478	A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018.)
|- ( P e. ( ( V WWalksN E ) ` N ) -> P e. ( V WWalks E ) )
Theorem	wwlksswwlkn 25479	The walks of a fixed length as words are walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 17-Jul-2018.)
|- ( ( V WWalksN E ) ` N ) C_ ( V WWalks E )
Theorem	wwlknimpb 25480	Basic implications for a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 3-Oct-2018.)
|- ( W e. ( ( V WWalksN E ) ` N ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) )
Theorem	wwlkn0s 25481*	The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( ( V WWalksN E ) ` 0 ) = { w e. Word V | ( # ` w ) = 1 } )
Theorem	vfwlkniswwlkn 25482	If the edge function of a walk has length n, then the vertex function of the walk is a word representing the walk as word of length n. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- ( ( N e. NN0 /\ ( W e. ( V Walks E ) /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( 2nd ` W ) e. ( ( V WWalksN E ) ` N ) )
Theorem	2wlkeq 25483*	Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.)
|- ( ( A e. ( V Walks E ) /\ B e. ( V Walks E ) /\ 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	usg2wlkeq 25484*	Conditions for two walks within the same undirected simple graph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.)
|- ( ( V USGrph E /\ ( A e. ( V Walks E ) /\ B e. ( V Walks E ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) ) )
Theorem	usg2wlkeq2 25485	Conditions for which two walks within the same undirected simple graph are the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- ( ( ( V USGrph E /\ N e. NN0 ) /\ ( X e. ( V Walks E ) /\ ( # ` ( 1st ` X ) ) = N ) /\ ( W e. ( V Walks E ) /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( ( 2nd ` X ) = ( 2nd ` W ) -> X = W ) )
Theorem	wlknwwlknfun 25486*	Lemma 1 for wlknwwlknbij2 25490. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- T = { p e. ( V Walks E ) | ( # ` ( 1st ` p ) ) = N }   &    |- W = ( ( V WWalksN E ) ` N )   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( N e. NN0 -> F : T --> W )
Theorem	wlknwwlkninj 25487*	Lemma 2 for wlknwwlknbij2 25490. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- T = { p e. ( V Walks E ) | ( # ` ( 1st ` p ) ) = N }   &    |- W = ( ( V WWalksN E ) ` N )   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( V USGrph E /\ N e. NN0 ) -> F : T -1-1-> W )
Theorem	wlknwwlknsur 25488*	Lemma 3 for wlknwwlknbij2 25490. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- T = { p e. ( V Walks E ) | ( # ` ( 1st ` p ) ) = N }   &    |- W = ( ( V WWalksN E ) ` N )   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( V USGrph E /\ N e. NN0 ) -> F : T -onto-> W )
Theorem	wlknwwlknbij 25489*	Lemma 4 for wlknwwlknbij2 25490. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- T = { p e. ( V Walks E ) | ( # ` ( 1st ` p ) ) = N }   &    |- W = ( ( V WWalksN E ) ` N )   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( V USGrph E /\ N e. NN0 ) -> F : T -1-1-onto-> W )
Theorem	wlknwwlknbij2 25490*	There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- ( ( V USGrph E /\ N e. NN0 ) -> E. f f : { p e. ( V Walks E ) | ( # ` ( 1st ` p ) ) = N } -1-1-onto-> ( ( V WWalksN E ) ` N ) )
Theorem	wlknwwlknen 25491*	The set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- ( ( V USGrph E /\ N e. NN0 ) -> { p e. ( V Walks E ) | ( # ` ( 1st ` p ) ) = N } ~~ ( ( V WWalksN E ) ` N ) )
Theorem	wlknwwlkneqs 25492*	The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- ( ( V USGrph E /\ N e. NN0 ) -> ( # ` { p e. ( V Walks E ) | ( # ` ( 1st ` p ) ) = N } ) = ( # ` ( ( V WWalksN E ) ` N ) ) )
Theorem	wlkiswwlkfun 25493*	Lemma 1 for wlkiswwlkbij2 25497. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.)
|- T = { p e. ( V Walks E ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) }   &    |- W = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( P e. V /\ N e. NN0 ) -> F : T --> W )
Theorem	wlkiswwlkinj 25494*	Lemma 2 for wlkiswwlkbij2 25497. (Contributed by Alexander van der Vekens, 23-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.)
|- T = { p e. ( V Walks E ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) }   &    |- W = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( V USGrph E /\ P e. V /\ N e. NN0 ) -> F : T -1-1-> W )
Theorem	wlkiswwlksur 25495*	Lemma 3 for wlkiswwlkbij2 25497. (Contributed by Alexander van der Vekens, 23-Jul-2018.)
|- T = { p e. ( V Walks E ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) }   &    |- W = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( V USGrph E /\ P e. V /\ N e. NN0 ) -> F : T -onto-> W )
Theorem	wlkiswwlkbij 25496*	Lemma 4 for wlkiswwlkbij2 25497. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- T = { p e. ( V Walks E ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) }   &    |- W = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( V USGrph E /\ P e. V /\ N e. NN0 ) -> F : T -1-1-onto-> W )
Theorem	wlkiswwlkbij2 25497*	There is a bijection between the set of walks of a fixed length, starting at a fixed vertex, and the set of walks represented as words of the same length, starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- ( ( V USGrph E /\ P e. V /\ N e. NN0 ) -> E. f f : { p e. ( V Walks E ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) } -1-1-onto-> { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P } )
Theorem	wwlkeq 25498*	Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018.)
|- ( ( W e. ( V WWalks E ) /\ T e. ( V WWalks E ) ) -> ( W = T <-> ( ( # ` W ) = ( # ` T ) /\ A. i e. ( 0..^ ( # ` W ) ) ( W ` i ) = ( T ` i ) ) ) )
Theorem	wwlknred 25499	Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.)
|- ( N e. NN0 -> ( W e. ( ( V WWalksN E ) ` ( N + 1 ) ) -> ( W substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) ) )
Theorem	wwlknext 25500	Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.)
|- ( ( T e. ( ( V WWalksN E ) ` N ) /\ S e. V /\ { ( lastS ` T ) , S } e. ran E ) -> ( T ++ <" S "> ) e. ( ( V WWalksN E ) ` ( N + 1 ) ) )