Metamath Proof Explorer

Theorem upgrwlkdvspth

Description: A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk . (Contributed by Alexander van der Vekens, 27-Oct-2017) (Revised by AV, 17-Jan-2021)

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

Proof

Step Hyp Ref Expression
1 3simpc 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> ( F ( Walks ` G ) P /\ Fun `' P ) )
2 upgrspthswlk 
 |-  ( G e. UPGraph -> ( SPaths ` G ) = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } )
3 2 3ad2ant1 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> ( SPaths ` G ) = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } )
4 3 breqd 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> ( F ( SPaths ` G ) P <-> F { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } P ) )
5 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
6 3simpc 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F e. _V /\ P e. _V ) )
7 5 6 syl 
 |-  ( F ( Walks ` G ) P -> ( F e. _V /\ P e. _V ) )
8 7 3ad2ant2 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> ( F e. _V /\ P e. _V ) )
9 breq12 
 |-  ( ( f = F /\ p = P ) -> ( f ( Walks ` G ) p <-> F ( Walks ` G ) P ) )
10 cnveq 
 |-  ( p = P -> `' p = `' P )
11 10 funeqd 
 |-  ( p = P -> ( Fun `' p <-> Fun `' P ) )
12 11 adantl 
 |-  ( ( f = F /\ p = P ) -> ( Fun `' p <-> Fun `' P ) )
13 9 12 anbi12d 
 |-  ( ( f = F /\ p = P ) -> ( ( f ( Walks ` G ) p /\ Fun `' p ) <-> ( F ( Walks ` G ) P /\ Fun `' P ) ) )
14 eqid 
 |-  { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) }
15 13 14 brabga 
 |-  ( ( F e. _V /\ P e. _V ) -> ( F { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } P <-> ( F ( Walks ` G ) P /\ Fun `' P ) ) )
16 8 15 syl 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> ( F { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } P <-> ( F ( Walks ` G ) P /\ Fun `' P ) ) )
17 4 16 bitrd 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> ( F ( SPaths ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' P ) ) )
18 1 17 mpbird 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> F ( SPaths ` G ) P )