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 G ) = { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 }

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 wwlksn 
 |-  ( 0 e. NN0 -> ( 0 WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( 0 + 1 ) } )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
5 3 4 iswwlks 
 |-  ( w e. ( WWalks ` G ) <-> ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
6 0p1e1 
 |-  ( 0 + 1 ) = 1
7 6 eqeq2i 
 |-  ( ( # ` w ) = ( 0 + 1 ) <-> ( # ` w ) = 1 )
8 5 7 anbi12i 
 |-  ( ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( 0 + 1 ) ) <-> ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = 1 ) )
9 simp2 
 |-  ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> w e. Word ( Vtx ` G ) )
10 vex 
 |-  w e. _V
11 0lt1 
 |-  0 < 1
12 breq2 
 |-  ( ( # ` w ) = 1 -> ( 0 < ( # ` w ) <-> 0 < 1 ) )
13 11 12 mpbiri 
 |-  ( ( # ` w ) = 1 -> 0 < ( # ` w ) )
14 hashgt0n0 
 |-  ( ( w e. _V /\ 0 < ( # ` w ) ) -> w =/= (/) )
15 10 13 14 sylancr 
 |-  ( ( # ` w ) = 1 -> w =/= (/) )
16 15 adantr 
 |-  ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) ) -> w =/= (/) )
17 simpr 
 |-  ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) ) -> w e. Word ( Vtx ` G ) )
18 ral0 
 |-  A. i e. (/) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G )
19 oveq1 
 |-  ( ( # ` w ) = 1 -> ( ( # ` w ) - 1 ) = ( 1 - 1 ) )
20 1m1e0 
 |-  ( 1 - 1 ) = 0
21 19 20 eqtrdi 
 |-  ( ( # ` w ) = 1 -> ( ( # ` w ) - 1 ) = 0 )
22 21 oveq2d 
 |-  ( ( # ` w ) = 1 -> ( 0 ..^ ( ( # ` w ) - 1 ) ) = ( 0 ..^ 0 ) )
23 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
24 22 23 eqtrdi 
 |-  ( ( # ` w ) = 1 -> ( 0 ..^ ( ( # ` w ) - 1 ) ) = (/) )
25 24 raleqdv 
 |-  ( ( # ` w ) = 1 -> ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. (/) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
26 18 25 mpbiri 
 |-  ( ( # ` w ) = 1 -> A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) )
27 26 adantr 
 |-  ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) ) -> A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) )
28 16 17 27 3jca 
 |-  ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) ) -> ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
29 28 ex 
 |-  ( ( # ` w ) = 1 -> ( w e. Word ( Vtx ` G ) -> ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
30 9 29 impbid2 
 |-  ( ( # ` w ) = 1 -> ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> w e. Word ( Vtx ` G ) ) )
31 30 pm5.32ri 
 |-  ( ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) /\ ( # ` w ) = 1 ) <-> ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) )
32 8 31 bitri 
 |-  ( ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( 0 + 1 ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) )
33 32 a1i 
 |-  ( 0 e. NN0 -> ( ( w e. ( WWalks ` G ) /\ ( # ` w ) = ( 0 + 1 ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = 1 ) ) )
34 33 rabbidva2 
 |-  ( 0 e. NN0 -> { w e. ( WWalks ` G ) | ( # ` w ) = ( 0 + 1 ) } = { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 } )
35 2 34 eqtrd 
 |-  ( 0 e. NN0 -> ( 0 WWalksN G ) = { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 } )
36 1 35 ax-mp 
 |-  ( 0 WWalksN G ) = { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 }