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

Metamath Proof Explorer

Theorem upgrspthswlk

Description: The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p_0, p_1, p_2 } be a hyperedge, then ( p_0, e, p_1, e, p_2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021) (Proof shortened by AV, 17-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion upgrspthswlk 
|- ( G e. UPGraph -> ( SPaths ` G ) = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } )

Proof

Step Hyp Ref Expression
1 spthsfval 
 |-  ( SPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) }
2 istrl 
 |-  ( f ( Trails ` G ) p <-> ( f ( Walks ` G ) p /\ Fun `' f ) )
3 upgrwlkdvde 
 |-  ( ( G e. UPGraph /\ f ( Walks ` G ) p /\ Fun `' p ) -> Fun `' f )
4 3 3exp 
 |-  ( G e. UPGraph -> ( f ( Walks ` G ) p -> ( Fun `' p -> Fun `' f ) ) )
5 4 com23 
 |-  ( G e. UPGraph -> ( Fun `' p -> ( f ( Walks ` G ) p -> Fun `' f ) ) )
6 5 imp 
 |-  ( ( G e. UPGraph /\ Fun `' p ) -> ( f ( Walks ` G ) p -> Fun `' f ) )
7 6 pm4.71d 
 |-  ( ( G e. UPGraph /\ Fun `' p ) -> ( f ( Walks ` G ) p <-> ( f ( Walks ` G ) p /\ Fun `' f ) ) )
8 2 7 bitr4id 
 |-  ( ( G e. UPGraph /\ Fun `' p ) -> ( f ( Trails ` G ) p <-> f ( Walks ` G ) p ) )
9 8 ex 
 |-  ( G e. UPGraph -> ( Fun `' p -> ( f ( Trails ` G ) p <-> f ( Walks ` G ) p ) ) )
10 9 pm5.32rd 
 |-  ( G e. UPGraph -> ( ( f ( Trails ` G ) p /\ Fun `' p ) <-> ( f ( Walks ` G ) p /\ Fun `' p ) ) )
11 10 opabbidv 
 |-  ( G e. UPGraph -> { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) } = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } )
12 1 11 eqtrid 
 |-  ( G e. UPGraph -> ( SPaths ` G ) = { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' p ) } )