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 }