This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0wlk

Description: A pair of an empty set (of edges) and a second set (of vertices) is a walk iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 3-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0wlk.v 
|- V = ( Vtx ` G )
Assertion 0wlk 
|- ( G e. U -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )

Proof

Step Hyp Ref Expression
1 0wlk.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 iswlkg 
 |-  ( G e. U -> ( (/) ( Walks ` G ) P <-> ( (/) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` (/) ) ) --> V /\ A. k e. ( 0 ..^ ( # ` (/) ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) ) )
4 ral0 
 |-  A. k e. (/) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) )
5 hash0 
 |-  ( # ` (/) ) = 0
6 5 oveq2i 
 |-  ( 0 ..^ ( # ` (/) ) ) = ( 0 ..^ 0 )
7 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
8 6 7 eqtri 
 |-  ( 0 ..^ ( # ` (/) ) ) = (/)
9 8 raleqi 
 |-  ( A. k e. ( 0 ..^ ( # ` (/) ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) ) <-> A. k e. (/) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) ) )
10 4 9 mpbir 
 |-  A. k e. ( 0 ..^ ( # ` (/) ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) )
11 10 biantru 
 |-  ( ( (/) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` (/) ) ) --> V ) <-> ( ( (/) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` (/) ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` (/) ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) )
12 5 eqcomi 
 |-  0 = ( # ` (/) )
13 12 oveq2i 
 |-  ( 0 ... 0 ) = ( 0 ... ( # ` (/) ) )
14 13 feq2i 
 |-  ( P : ( 0 ... 0 ) --> V <-> P : ( 0 ... ( # ` (/) ) ) --> V )
15 wrd0 
 |-  (/) e. Word dom ( iEdg ` G )
16 15 biantrur 
 |-  ( P : ( 0 ... ( # ` (/) ) ) --> V <-> ( (/) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` (/) ) ) --> V ) )
17 14 16 bitri 
 |-  ( P : ( 0 ... 0 ) --> V <-> ( (/) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` (/) ) ) --> V ) )
18 df-3an 
 |-  ( ( (/) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` (/) ) ) --> V /\ A. k e. ( 0 ..^ ( # ` (/) ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) <-> ( ( (/) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` (/) ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` (/) ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) )
19 11 17 18 3bitr4ri 
 |-  ( ( (/) e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` (/) ) ) --> V /\ A. k e. ( 0 ..^ ( # ` (/) ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( (/) ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( (/) ` k ) ) ) ) <-> P : ( 0 ... 0 ) --> V )
20 3 19 bitrdi 
 |-  ( G e. U -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )