This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )