Metamath Proof Explorer

Theorem upgrwlkdvde

Description: In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk . (Contributed by AV, 17-Jan-2021)

Ref Expression
Assertion upgrwlkdvde 
|- ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> Fun `' F )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
4 df-f1 
 |-  ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) <-> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' P ) )
5 4 simplbi2 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( Fun `' P -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) )
6 5 3ad2ant2 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( Fun `' P -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) )
7 6 impcom 
 |-  ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )
8 simpr1 
 |-  ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> F e. Word dom ( iEdg ` G ) )
9 7 8 jca 
 |-  ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ F e. Word dom ( iEdg ` G ) ) )
10 simpr3 
 |-  ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
11 upgrwlkdvdelem 
 |-  ( ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ F e. Word dom ( iEdg ` G ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> Fun `' F ) )
12 9 10 11 sylc 
 |-  ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> Fun `' F )
13 12 expcom 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( Fun `' P -> Fun `' F ) )
14 3 13 syl6bi 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P -> ( Fun `' P -> Fun `' F ) ) )
15 14 3imp 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> Fun `' F )