P. 401 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40001-40100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	crctcshtrl 40001*	Cyclically shifting the indices of a circuit <. F , P >. results in a trail <. H , Q >.. (Contributed by AV, 14-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (CircuitS ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ph -> H (TrailS ` G ) Q )
Theorem	crctcsh 40002*	Cyclically shifting the indices of a circuit <. F , P >. results in a circuit <. H , Q >.. (Contributed by AV, 10-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (CircuitS ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ph -> H (CircuitS ` G ) Q )
21.33.8.20  Examples for walks, trails and paths
Theorem	0ewlk 40003	The empty set (empty sequence of edges) is an s-walk of edges for all s. (Contributed by AV, 4-Jan-2021.)
|- ( ( G e. _V /\ S e. NN0* ) -> (/) e. ( G EdgWalks S ) )
Theorem	1ewlk 40004	A sequence of 1 edge is an s-walk of edges for all s. (Contributed by AV, 5-Jan-2021.)
|- ( ( G e. _V /\ S e. NN0* /\ I e. dom (iEdg ` G ) ) -> <" I "> e. ( G EdgWalks S ) )
Theorem	01wlk 40005	A pair of an empty set (of edges) and a second set (of vertices) is a walk iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 3-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. U /\ P e. Z ) -> ( (/) (1Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
Theorem	is01wlklem 40006	Lemma for is01wlk 40007 and is0Trl 40012. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( ( P = { <. 0 , N >. } /\ N e. V ) -> P : ( 0 ... 0 ) --> V )
Theorem	is01wlk 40007	A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( ( P = { <. 0 , N >. } /\ N e. V ) -> (/) (1Walks ` G ) P )
Theorem	0wlkOnlem1 40008	Lemma 1 for 0wlkOn 40010 and 0TrlOn 40013. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( N e. V /\ N e. V ) )
Theorem	0wlkOnlem2 40009	Lemma 2 for 0wlkOn 40010 and 0TrlOn 40013. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> P e. ( V ^pm ( 0 ... 0 ) ) )
Theorem	0wlkOn 40010	A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N (WalksOn ` G ) N ) P )
Theorem	0Trl 40011	A pair of an empty set (of edges) and a second set (of vertices) is a trail iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 7-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. U /\ P e. Z ) -> ( (/) (TrailS ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
Theorem	is0Trl 40012	A pair of an empty set (of edges) and a sequence of one vertex is a trail (of length 0). (Contributed by AV, 7-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( ( P = { <. 0 , N >. } /\ N e. V ) -> (/) (TrailS ` G ) P )
Theorem	0TrlOn 40013	A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 8-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- V = (Vtx ` G )   =>    |- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N (TrailsOn ` G ) N ) P )
Theorem	0pth-av 40014	A pair of an empty set (of edges) and a second set (of vertices) is a path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 19-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ P e. Z ) -> ( (/) (PathS ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
Theorem	0spth-av 40015	A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 18-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ P e. Z ) -> ( (/) (SPathS ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
Theorem	0pthon-av 40016	A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( N e. V -> ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N (PathsOn ` G ) N ) P ) )
Theorem	0pthon1-av 40017	A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( N e. V -> (/) ( N (PathsOn ` G ) N ) { <. 0 , N >. } )
Theorem	0pthonv-av 40018*	For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 21-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( N e. V -> E. f E. p f ( N (PathsOn ` G ) N ) p )
Theorem	0clWlk 40019	A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 17-Feb-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. X /\ P e. Z ) -> ( (/) (ClWalkS ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
Theorem	0clwlk0 40020	There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- (ClWalkS ` (/) ) = (/)
Theorem	0Crct 40021	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.) (Revised by AV, 31-Jan-2021.)
|- ( ( G e. W /\ P e. Z ) -> ( (/) (CircuitS ` G ) P <-> P : ( 0 ... 0 ) --> (Vtx ` G ) ) )
Theorem	0Cycl 40022	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.) (Revised by AV, 31-Jan-2021.)
|- ( ( G e. W /\ P e. Z ) -> ( (/) (CycleS ` G ) P <-> P : ( 0 ... 0 ) --> (Vtx ` G ) ) )
Theorem	1pthdlem1 40023	Lemma 1 for 1pthd 40031. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   =>    |- Fun `' ( P |` ( 1..^ ( # ` F ) ) )
Theorem	1pthdlem2 40024	Lemma 2 for 1pthd 40031. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   =>    |- ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1..^ ( # ` F ) ) ) ) = (/)
Theorem	11wlkdlem1 40025	Lemma 1 for 11wlkd 40029. (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
Theorem	11wlkdlem2 40026	Lemma 2 for 11wlkd 40029. (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )   &    |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )   =>    |- ( ph -> X e. ( I ` J ) )
Theorem	11wlkdlem3 40027	Lemma 3 for 11wlkd 40029. (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )   &    |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )   =>    |- ( ph -> F e. Word dom I )
Theorem	11wlkdlem4 40028*	Lemma 4 for 11wlkd 40029. (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )   &    |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )   =>    |- ( ph -> 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	11wlkd 40029	In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )   &    |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ph -> F (1Walks ` G ) P )
Theorem	1trld 40030	In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )   &    |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ph -> F (TrailS ` G ) P )
Theorem	1pthd 40031	In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )   &    |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ph -> F (PathS ` G ) P )
Theorem	1pthond 40032	In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )   &    |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ph -> F ( X (PathsOn ` G ) Y ) P )
Theorem	upgr11wlkdlem1 40033	Lemma 1 for upgr11wlkd 40035. (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. (Vtx ` G ) )   &    |- ( ph -> Y e. (Vtx ` G ) )   &    |- ( ph -> ( (iEdg ` G ) ` J ) = { X , Y } )   =>    |- ( ( ph /\ X = Y ) -> ( (iEdg ` G ) ` J ) = { X } )
Theorem	upgr11wlkdlem2 40034	Lemma 2 for upgr11wlkd 40035. (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. (Vtx ` G ) )   &    |- ( ph -> Y e. (Vtx ` G ) )   &    |- ( ph -> ( (iEdg ` G ) ` J ) = { X , Y } )   =>    |- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( (iEdg ` G ) ` J ) )
Theorem	upgr11wlkd 40035	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. (Vtx ` G ) )   &    |- ( ph -> Y e. (Vtx ` G ) )   &    |- ( ph -> ( (iEdg ` G ) ` J ) = { X , Y } )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> F (1Walks ` G ) P )
Theorem	upgr1trld 40036	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. (Vtx ` G ) )   &    |- ( ph -> Y e. (Vtx ` G ) )   &    |- ( ph -> ( (iEdg ` G ) ` J ) = { X , Y } )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> F (TrailS ` G ) P )
Theorem	upgr1pthd 40037	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. (Vtx ` G ) )   &    |- ( ph -> Y e. (Vtx ` G ) )   &    |- ( ph -> ( (iEdg ` G ) ` J ) = { X , Y } )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> F (PathS ` G ) P )
Theorem	upgr1pthond 40038	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.)
|- P = <" X Y ">   &    |- F = <" J ">   &    |- ( ph -> X e. (Vtx ` G ) )   &    |- ( ph -> Y e. (Vtx ` G ) )   &    |- ( ph -> ( (iEdg ` G ) ` J ) = { X , Y } )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> F ( X (PathsOn ` G ) Y ) P )
Theorem	lppthon 40039	A loop (which is an edge at index J) induces a path of length 1 from a vertex to itself in a hypergraph. (Contributed by AV, 1-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( A (PathsOn ` G ) A ) <" A A "> )
Theorem	lp1cycl 40040	A loop (which is an edge at index J) induces a cycle of length 1 in a hypergraph. (Contributed by AV, 2-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> (CycleS ` G ) <" A A "> )
Theorem	1pthon2v-av 40041*	For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) -> E. f E. p f ( A (PathsOn ` G ) B ) p )
Theorem	1pthon2ve 40042*	For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Proof shortened by AV, 15-Feb-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ { A , B } e. E ) -> E. f E. p f ( A (PathsOn ` G ) B ) p )
Theorem	1wlk2v2elem1 40043	Lemma 1 for 1wlk2v2e 40045: F is a length 2 word of over { 0 }, the domain of the singleton word I. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.)
|- I = <" { X , Y } ">   &    |- F = <" 0 0 ">   =>    |- F e. Word dom I
Theorem	1wlk2v2elem2 40044*	Lemma 2 for 1wlk2v2e 40045: The values of I after F are edges between two vertices enumerated by P. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.)
|- I = <" { X , Y } ">   &    |- F = <" 0 0 ">   &    |- X e. _V   &    |- Y e. _V   &    |- P = <" X Y X ">   =>    |- A. k e. ( 0..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) }
Theorem	1wlk2v2e 40045	In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk. Notice that G is a simple graph (without loops) only if X =/= Y. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.)
|- I = <" { X , Y } ">   &    |- F = <" 0 0 ">   &    |- X e. _V   &    |- Y e. _V   &    |- P = <" X Y X ">   &    |- G = <. { X , Y } , I >.   =>    |- F (1Walks ` G ) P
Theorem	ntrl2v2e 40046	A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk, see 1wlk2v2e 40045, but not a trail. Notice that G is a simple graph (without loops) only if X =/= Y. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.)
|- I = <" { X , Y } ">   &    |- F = <" 0 0 ">   &    |- X e. _V   &    |- Y e. _V   &    |- P = <" X Y X ">   &    |- G = <. { X , Y } , I >.   =>    |- -. F (TrailS ` G ) P
Theorem	21wlkdlem1 40047	Lemma 1 for 21wlkd 40058. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   =>    |- ( # ` P ) = ( ( # ` F ) + 1 )
Theorem	21wlkdlem2 40048	Lemma 2 for 21wlkd 40058. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   =>    |- ( 0..^ ( # ` F ) ) = { 0 , 1 }
Theorem	21wlkdlem3 40049	Lemma 3 for 21wlkd 40058. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   =>    |- ( ph -> ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) )
Theorem	21wlkdlem4 40050*	Lemma 4 for 21wlkd 40058. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   =>    |- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )
Theorem	21wlkdlem5 40051*	Lemma 5 for 21wlkd 40058. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   =>    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
Theorem	2pthdlem1 40052*	Lemma 1 for 2pthd 40062. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   =>    |- ( ph -> A. k e. ( 0..^ ( # ` P ) ) A. j e. ( 1..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) )
Theorem	21wlkdlem6 40053	Lemma 6 for 21wlkd 40058. (Contributed by AV, 23-Jan-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   =>    |- ( ph -> ( B e. ( I ` J ) /\ B e. ( I ` K ) ) )
Theorem	21wlkdlem7 40054	Lemma 7 for 21wlkd 40058. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   =>    |- ( ph -> ( J e. _V /\ K e. _V ) )
Theorem	21wlkdlem8 40055	Lemma 8 for 21wlkd 40058. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   =>    |- ( ph -> ( ( F ` 0 ) = J /\ ( F ` 1 ) = K ) )
Theorem	21wlkdlem9 40056	Lemma 9 for 21wlkd 40058. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   =>    |- ( ph -> ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) ) )
Theorem	21wlkdlem10 40057*	Lemma 10 for 31wlkd 40084. (Contributed by AV, 14-Feb-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   =>    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
Theorem	21wlkd 40058	Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018.) (Revised by AV, 23-Jan-2021.) (Proof shortened by AV, 14-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ph -> F (1Walks ` G ) P )
Theorem	21wlkond 40059	A 1-walk of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ph -> F ( A (WalksOn ` G ) C ) P )
Theorem	2trld 40060	Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> J =/= K )   =>    |- ( ph -> F (TrailS ` G ) P )
Theorem	2trlond 40061	A trail of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> J =/= K )   =>    |- ( ph -> F ( A (TrailsOn ` G ) C ) P )
Theorem	2pthd 40062	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 AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> J =/= K )   =>    |- ( ph -> F (PathS ` G ) P )
Theorem	2spthd 40063	A simple path of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> J =/= K )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> F (SPathS ` G ) P )
Theorem	2pthond 40064	A simple path of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 24-Jan-2021.) (Proof shortened by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C ">   &    |- F = <" J K ">   &    |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )   &    |- ( ph -> ( A =/= B /\ B =/= C ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> J =/= K )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> F ( A (SPathsOn ` G ) C ) P )
Theorem	2pthon3v-av 40065*	For a vertex adjacent to two other vertices there is a simple path of length 2 between these other vertices in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 24-Jan-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( { A , B } e. E /\ { B , C } e. E ) ) -> E. f E. p ( f ( A (SPathsOn ` G ) C ) p /\ ( # ` f ) = 2 ) )
Theorem	umgr2adedgwlklem 40066	Lemma for umgr2adedgwlk 40067, umgr2adedgspth 40070, etc. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.)
|- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( ( A =/= B /\ B =/= C ) /\ ( A e. (Vtx ` G ) /\ B e. (Vtx ` G ) /\ C e. (Vtx ` G ) ) ) )
Theorem	umgr2adedgwlk 40067	In a multigraph, two adjacent edges form a walk of length 2. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 29-Jan-2021.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- F = <" J K ">   &    |- P = <" A B C ">   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )   &    |- ( ph -> ( I ` J ) = { A , B } )   &    |- ( ph -> ( I ` K ) = { B , C } )   =>    |- ( ph -> ( F (1Walks ` G ) P /\ ( # ` F ) = 2 /\ ( A = ( P ` 0 ) /\ B = ( P ` 1 ) /\ C = ( P ` 2 ) ) ) )
Theorem	umgr2adedgwlkon 40068	In a multigraph, two adjacent edges form a walk between two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- F = <" J K ">   &    |- P = <" A B C ">   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )   &    |- ( ph -> ( I ` J ) = { A , B } )   &    |- ( ph -> ( I ` K ) = { B , C } )   =>    |- ( ph -> F ( A (WalksOn ` G ) C ) P )
Theorem	umgr2adedgwlkonALT 40069	Alternate proof for umgr2adedgwlkon 40068, using umgr2adedgwlk 40067, but with a much longer proof! In a multigraph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- F = <" J K ">   &    |- P = <" A B C ">   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )   &    |- ( ph -> ( I ` J ) = { A , B } )   &    |- ( ph -> ( I ` K ) = { B , C } )   =>    |- ( ph -> F ( A (WalksOn ` G ) C ) P )
Theorem	umgr2adedgspth 40070	In a multigraph, two adjacent edges with different endvertices form a simple path of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.)
|- E = (Edg ` G )   &    |- I = (iEdg ` G )   &    |- F = <" J K ">   &    |- P = <" A B C ">   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )   &    |- ( ph -> ( I ` J ) = { A , B } )   &    |- ( ph -> ( I ` K ) = { B , C } )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> F (SPathS ` G ) P )
Theorem	umgr2wlk 40071*	In a multigraph, there is a 1-walk of length 2 for each pair of adjacent edges. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.)
|- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. f E. p ( f (1Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) )
Theorem	umgr2wlkon 40072*	For each pair of adjacent edges in a multigraph, there is a 1-walk of length 2 between the not common vertices of the edges. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.)
|- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. f E. p f ( A (WalksOn ` G ) C ) p )
Theorem	31wlkdlem1 40073	Lemma 1 for 31wlkd 40084. (Contributed by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   =>    |- ( # ` P ) = ( ( # ` F ) + 1 )
Theorem	31wlkdlem2 40074	Lemma 2 for 31wlkd 40084. (Contributed by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   =>    |- ( 0..^ ( # ` F ) ) = { 0 , 1 , 2 }
Theorem	31wlkdlem3 40075	Lemma 3 for 31wlkd 40084. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   =>    |- ( ph -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) )
Theorem	31wlkdlem4 40076*	Lemma 4 for 31wlkd 40084. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   =>    |- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )
Theorem	31wlkdlem5 40077*	Lemma 5 for 31wlkd 40084. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   =>    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
Theorem	3pthdlem1 40078*	Lemma 1 for 3pthd 40088. (Contributed by AV, 9-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   =>    |- ( ph -> A. k e. ( 0..^ ( # ` P ) ) A. j e. ( 1..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) )
Theorem	31wlkdlem6 40079	Lemma 6 for 31wlkd 40084. (Contributed by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   =>    |- ( ph -> ( A e. ( I ` J ) /\ B e. ( I ` K ) /\ C e. ( I ` L ) ) )
Theorem	31wlkdlem7 40080	Lemma 7 for 31wlkd 40084. (Contributed by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   =>    |- ( ph -> ( J e. _V /\ K e. _V /\ L e. _V ) )
Theorem	31wlkdlem8 40081	Lemma 8 for 31wlkd 40084. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   =>    |- ( ph -> ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) )
Theorem	31wlkdlem9 40082	Lemma 9 for 31wlkd 40084. (Contributed by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   =>    |- ( ph -> ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) /\ { C , D } C_ ( I ` ( F ` 2 ) ) ) )
Theorem	31wlkdlem10 40083*	Lemma 10 for 31wlkd 40084. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   =>    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
Theorem	31wlkd 40084	Construction of a walk from two given edges in a graph. (Contributed by AV, 7-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ph -> F (1Walks ` G ) P )
Theorem	31wlkond 40085	A 1-walk of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ph -> F ( A (WalksOn ` G ) D ) P )
Theorem	3trld 40086	Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )   =>    |- ( ph -> F (TrailS ` G ) P )
Theorem	3trlond 40087	A trail of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )   =>    |- ( ph -> F ( A (TrailsOn ` G ) D ) P )
Theorem	3pthd 40088	A path of length 3 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )   =>    |- ( ph -> F (PathS ` G ) P )
Theorem	3pthond 40089	A path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )   =>    |- ( ph -> F ( A (PathsOn ` G ) D ) P )
Theorem	3spthd 40090	A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )   &    |- ( ph -> A =/= D )   =>    |- ( ph -> F (SPathS ` G ) P )
Theorem	3spthond 40091	A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )   &    |- ( ph -> A =/= D )   =>    |- ( ph -> F ( A (SPathsOn ` G ) D ) P )
Theorem	3cycld 40092	Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )   &    |- ( ph -> A = D )   =>    |- ( ph -> F (CycleS ` G ) P )
Theorem	3cyclpd 40093	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.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.)
|- P = <" A B C D ">   &    |- F = <" J K L ">   &    |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )   &    |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )   &    |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )   &    |- ( ph -> A = D )   =>    |- ( ph -> ( F (CycleS ` G ) P /\ ( # ` F ) = 3 /\ ( P ` 0 ) = A ) )
Theorem	upgr3v3e3cycl 40094*	If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
|- E = (Edg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. UPGraph /\ F (CycleS ` G ) P /\ ( # ` F ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) )
Theorem	uhgr3cyclexlem 40095	Lemma for uhgr3cyclex 40096. (Contributed by AV, 12-Feb-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( ( ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( J e. dom I /\ { B , C } = ( I ` J ) ) /\ ( K e. dom I /\ { C , A } = ( I ` K ) ) ) ) -> J =/= K )
Theorem	uhgr3cyclex 40096*	If there are three different vertices in a hypergraph 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.) (Revised by AV, 12-Feb-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E. f E. p ( f (CycleS ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )
Theorem	umgr3cyclex 40097*	If there are three (different) vertices in a multigraph 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.) (Revised by AV, 12-Feb-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E. f E. p ( f (CycleS ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )
Theorem	umgr3v3e3cycl 40098*	If and only if there is a 3-cycle in a multigraph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.) (Revised by AV, 12-Feb-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. UMGraph -> ( E. f E. p ( f (CycleS ` G ) p /\ ( # ` f ) = 3 ) <-> E. a e. V E. b e. V E. c e. V ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) ) )
Theorem	upgr4cycl4dv4e 40099*	If there is a cycle of length 4 in a pseudograph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 13-Feb-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ F (CycleS ` G ) P /\ ( # ` F ) = 4 ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )
21.33.8.21  Connected graphs
Syntax	cconngr 40100	Extend class notation with connected graphs.
class ConnGraph