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 )