Metamath Proof Explorer

Theorem lfgrwlknloop

Description: In a loop-free graph, each walk has no loops! (Contributed by AV, 2-Feb-2021)

Ref Expression
Hypotheses lfgrwlkprop.i 
|- I = ( iEdg ` G )
lfgriswlk.v 
|- V = ( Vtx ` G )
Assertion lfgrwlknloop 
|- ( ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )

Proof

Step Hyp Ref Expression
1 lfgrwlkprop.i 
 |-  I = ( iEdg ` G )
2 lfgriswlk.v 
 |-  V = ( Vtx ` G )
3 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
4 1 2 lfgriswlk 
 |-  ( ( G e. _V /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
5 simpl 
 |-  ( ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) )
6 5 ralimi 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
7 6 3ad2ant3 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
8 4 7 biimtrdi 
 |-  ( ( G e. _V /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
9 8 ex 
 |-  ( G e. _V -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
10 9 com23 
 |-  ( G e. _V -> ( F ( Walks ` G ) P -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
11 10 3ad2ant1 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
12 3 11 mpcom 
 |-  ( F ( Walks ` G ) P -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
13 12 impcom 
 |-  ( ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )