Metamath Proof Explorer


Theorem wwlksn0s

Description: The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 12-Apr-2021)

Ref Expression
Assertion wwlksn0s ( 0 WWalksN 𝐺 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 1 }

Proof

Step Hyp Ref Expression
1 0nn0 0 ∈ ℕ0
2 wwlksn ( 0 ∈ ℕ0 → ( 0 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 0 + 1 ) } )
3 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
5 3 4 iswwlks ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
6 0p1e1 ( 0 + 1 ) = 1
7 6 eqeq2i ( ( ♯ ‘ 𝑤 ) = ( 0 + 1 ) ↔ ( ♯ ‘ 𝑤 ) = 1 )
8 5 7 anbi12i ( ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 0 + 1 ) ) ↔ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) )
9 simp2 ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
10 vex 𝑤 ∈ V
11 0lt1 0 < 1
12 breq2 ( ( ♯ ‘ 𝑤 ) = 1 → ( 0 < ( ♯ ‘ 𝑤 ) ↔ 0 < 1 ) )
13 11 12 mpbiri ( ( ♯ ‘ 𝑤 ) = 1 → 0 < ( ♯ ‘ 𝑤 ) )
14 hashgt0n0 ( ( 𝑤 ∈ V ∧ 0 < ( ♯ ‘ 𝑤 ) ) → 𝑤 ≠ ∅ )
15 10 13 14 sylancr ( ( ♯ ‘ 𝑤 ) = 1 → 𝑤 ≠ ∅ )
16 15 adantr ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) → 𝑤 ≠ ∅ )
17 simpr ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
18 ral0 𝑖 ∈ ∅ { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 )
19 oveq1 ( ( ♯ ‘ 𝑤 ) = 1 → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( 1 − 1 ) )
20 1m1e0 ( 1 − 1 ) = 0
21 19 20 eqtrdi ( ( ♯ ‘ 𝑤 ) = 1 → ( ( ♯ ‘ 𝑤 ) − 1 ) = 0 )
22 21 oveq2d ( ( ♯ ‘ 𝑤 ) = 1 → ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ( 0 ..^ 0 ) )
23 fzo0 ( 0 ..^ 0 ) = ∅
24 22 23 eqtrdi ( ( ♯ ‘ 𝑤 ) = 1 → ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ∅ )
25 24 raleqdv ( ( ♯ ‘ 𝑤 ) = 1 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ∅ { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
26 18 25 mpbiri ( ( ♯ ‘ 𝑤 ) = 1 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
27 26 adantr ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
28 16 17 27 3jca ( ( ( ♯ ‘ 𝑤 ) = 1 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
29 28 ex ( ( ♯ ‘ 𝑤 ) = 1 → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
30 9 29 impbid2 ( ( ♯ ‘ 𝑤 ) = 1 → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ) )
31 30 pm5.32ri ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) )
32 8 31 bitri ( ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 0 + 1 ) ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) )
33 32 a1i ( 0 ∈ ℕ0 → ( ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 0 + 1 ) ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ) )
34 33 rabbidva2 ( 0 ∈ ℕ0 → { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 0 + 1 ) } = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 1 } )
35 2 34 eqtrd ( 0 ∈ ℕ0 → ( 0 WWalksN 𝐺 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 1 } )
36 1 35 ax-mp ( 0 WWalksN 𝐺 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 1 }