Theorem wwlks

Description: The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

	Ref	Expression
Hypotheses	wwlks.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	wwlks.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	wwlks	⊢ ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) }

Proof

Step	Hyp	Ref	Expression
1		wwlks.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		wwlks.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		df-wwlks	⊢ WWalks = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } )
4		fveq2	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
5	4 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
6		wrdeq	⊢ ( ( Vtx ‘ 𝑔 ) = 𝑉 → Word ( Vtx ‘ 𝑔 ) = Word 𝑉 )
7	5 6	syl	⊢ ( 𝑔 = 𝐺 → Word ( Vtx ‘ 𝑔 ) = Word 𝑉 )
8		fveq2	⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝐺 ) )
9	8 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = 𝐸 )
10	9	eleq2d	⊢ ( 𝑔 = 𝐺 → ( { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ↔ { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
11	10	ralbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
12	11	anbi2d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
13	7 12	rabeqbidv	⊢ ( 𝑔 = 𝐺 → { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } )
14		id	⊢ ( 𝐺 ∈ V → 𝐺 ∈ V )
15	1	fvexi	⊢ 𝑉 ∈ V
16	15	a1i	⊢ ( 𝐺 ∈ V → 𝑉 ∈ V )
17		wrdexg	⊢ ( 𝑉 ∈ V → Word 𝑉 ∈ V )
18		rabexg	⊢ ( Word 𝑉 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ∈ V )
19	16 17 18	3syl	⊢ ( 𝐺 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ∈ V )
20	3 13 14 19	fvmptd3	⊢ ( 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } )
21		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = ∅ )
22		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = ∅ )
23	1 22	syl5eq	⊢ ( ¬ 𝐺 ∈ V → 𝑉 = ∅ )
24		wrdeq	⊢ ( 𝑉 = ∅ → Word 𝑉 = Word ∅ )
25	23 24	syl	⊢ ( ¬ 𝐺 ∈ V → Word 𝑉 = Word ∅ )
26	25	eleq2d	⊢ ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉 ↔ 𝑤 ∈ Word ∅ ) )
27		0wrd0	⊢ ( 𝑤 ∈ Word ∅ ↔ 𝑤 = ∅ )
28	26 27	bitrdi	⊢ ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉 ↔ 𝑤 = ∅ ) )
29		nne	⊢ ( ¬ 𝑤 ≠ ∅ ↔ 𝑤 = ∅ )
30	29	biimpri	⊢ ( 𝑤 = ∅ → ¬ 𝑤 ≠ ∅ )
31	30	intnanrd	⊢ ( 𝑤 = ∅ → ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
32	28 31	syl6bi	⊢ ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉 → ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) )
33	32	ralrimiv	⊢ ( ¬ 𝐺 ∈ V → ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
34		rabeq0	⊢ ( { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } = ∅ ↔ ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
35	33 34	sylibr	⊢ ( ¬ 𝐺 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } = ∅ )
36	21 35	eqtr4d	⊢ ( ¬ 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } )
37	20 36	pm2.61i	⊢ ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) }