Theorem iswwlks

Description: A word over the set of vertices representing a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

	Ref	Expression
Hypotheses	wwlks.v	|- V = ( Vtx ` G )
	wwlks.e	|- E = ( Edg ` G )
Assertion	iswwlks	|- ( W e. ( WWalks ` G ) <-> ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		wwlks.v	|- V = ( Vtx ` G )
2		wwlks.e	|- E = ( Edg ` G )
3		neeq1	|- ( w = W -> ( w =/= (/) <-> W =/= (/) ) )
4		fveq2	|- ( w = W -> ( # ` w ) = ( # ` W ) )
5	4	oveq1d	|- ( w = W -> ( ( # ` w ) - 1 ) = ( ( # ` W ) - 1 ) )
6	5	oveq2d	|- ( w = W -> ( 0 ..^ ( ( # ` w ) - 1 ) ) = ( 0 ..^ ( ( # ` W ) - 1 ) ) )
7		fveq1	|- ( w = W -> ( w ` i ) = ( W ` i ) )
8		fveq1	|- ( w = W -> ( w ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
9	7 8	preq12d	|- ( w = W -> { ( w ` i ) , ( w ` ( i + 1 ) ) } = { ( W ` i ) , ( W ` ( i + 1 ) ) } )
10	9	eleq1d	|- ( w = W -> ( { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E <-> { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
11	6 10	raleqbidv	|- ( w = W -> ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
12	3 11	anbi12d	|- ( w = W -> ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) <-> ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
13	12	elrab	|- ( W e. { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } <-> ( W e. Word V /\ ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
14	1 2	wwlks	|- ( WWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) }
15	14	eleq2i	|- ( W e. ( WWalks ` G ) <-> W e. { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) } )
16		3anan12	|- ( ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) <-> ( W e. Word V /\ ( W =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) )
17	13 15 16	3bitr4i	|- ( W e. ( WWalks ` G ) <-> ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )