Metamath Proof Explorer

Theorem 0ewlk

Description: The empty set (empty sequence of edges) is an s-walk of edges for all s. (Contributed by AV, 4-Jan-2021)

Ref Expression
Assertion 0ewlk 
|- ( ( G e. _V /\ S e. NN0* ) -> (/) e. ( G EdgWalks S ) )

Proof

Step Hyp Ref Expression
1 wrd0 
 |-  (/) e. Word dom ( iEdg ` G )
2 ral0 
 |-  A. k e. (/) S <_ ( # ` ( ( ( iEdg ` G ) ` ( (/) ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( (/) ` k ) ) ) )
3 hash0 
 |-  ( # ` (/) ) = 0
4 3 oveq2i 
 |-  ( 1 ..^ ( # ` (/) ) ) = ( 1 ..^ 0 )
5 0le1 
 |-  0 <_ 1
6 1z 
 |-  1 e. ZZ
7 0z 
 |-  0 e. ZZ
8 fzon 
 |-  ( ( 1 e. ZZ /\ 0 e. ZZ ) -> ( 0 <_ 1 <-> ( 1 ..^ 0 ) = (/) ) )
9 6 7 8 mp2an 
 |-  ( 0 <_ 1 <-> ( 1 ..^ 0 ) = (/) )
10 5 9 mpbi 
 |-  ( 1 ..^ 0 ) = (/)
11 4 10 eqtri 
 |-  ( 1 ..^ ( # ` (/) ) ) = (/)
12 11 raleqi 
 |-  ( A. k e. ( 1 ..^ ( # ` (/) ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( (/) ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) <-> A. k e. (/) S <_ ( # ` ( ( ( iEdg ` G ) ` ( (/) ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) )
13 2 12 mpbir 
 |-  A. k e. ( 1 ..^ ( # ` (/) ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( (/) ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( (/) ` k ) ) ) )
14 1 13 pm3.2i 
 |-  ( (/) e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` (/) ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( (/) ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) )
15 0ex 
 |-  (/) e. _V
16 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
17 16 isewlk 
 |-  ( ( G e. _V /\ S e. NN0* /\ (/) e. _V ) -> ( (/) e. ( G EdgWalks S ) <-> ( (/) e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` (/) ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( (/) ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) ) ) )
18 15 17 mp3an3 
 |-  ( ( G e. _V /\ S e. NN0* ) -> ( (/) e. ( G EdgWalks S ) <-> ( (/) e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` (/) ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( (/) ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) ) ) )
19 14 18 mpbiri 
 |-  ( ( G e. _V /\ S e. NN0* ) -> (/) e. ( G EdgWalks S ) )