Metamath Proof Explorer

Theorem clwwlk

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

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

Proof

Step Hyp Ref Expression
1 clwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clwwlk.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 df-clwwlk ⊢ ClWWalks = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( 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 9 eleq2d ⊢ ( 𝑔 = 𝐺 → ( { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 ) ↔ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) )
13 11 12 3anbi23d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) ) )
14 7 13 rabeqbidv ⊢ ( 𝑔 = 𝐺 → { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 ) ) } = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } )
15 id ⊢ ( 𝐺 ∈ V → 𝐺 ∈ V )
16 1 fvexi ⊢ 𝑉 ∈ V
17 16 a1i ⊢ ( 𝐺 ∈ V → 𝑉 ∈ V )
18 wrdexg ⊢ ( 𝑉 ∈ V → Word 𝑉 ∈ V )
19 rabexg ⊢ ( Word 𝑉 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } ∈ V )
20 17 18 19 3syl ⊢ ( 𝐺 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } ∈ V )
21 3 14 15 20 fvmptd3 ⊢ ( 𝐺 ∈ V → ( ClWWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } )
22 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( ClWWalks ‘ 𝐺 ) = ∅ )
23 noel ⊢ ¬ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ∅
24 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Edg ‘ 𝐺 ) = ∅ )
25 2 24 syl5eq ⊢ ( ¬ 𝐺 ∈ V → 𝐸 = ∅ )
26 25 eleq2d ⊢ ( ¬ 𝐺 ∈ V → ( { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ∅ ) )
27 23 26 mtbiri ⊢ ( ¬ 𝐺 ∈ V → ¬ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 )
28 27 adantr ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑤 ∈ Word 𝑉 ) → ¬ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 )
29 28 intn3an3d ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑤 ∈ Word 𝑉 ) → ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) )
30 29 ralrimiva ⊢ ( ¬ 𝐺 ∈ V → ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) )
31 rabeq0 ⊢ ( { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } = ∅ ↔ ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) )
32 30 31 sylibr ⊢ ( ¬ 𝐺 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } = ∅ )
33 22 32 eqtr4d ⊢ ( ¬ 𝐺 ∈ V → ( ClWWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } )
34 21 33 pm2.61i ⊢ ( ClWWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) }