Metamath Proof Explorer


Theorem spthsfval

Description: The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion spthsfval
|- ( SPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) }

Proof

Step Hyp Ref Expression
1 biidd
 |-  ( ( T. /\ g = G ) -> ( Fun `' p <-> Fun `' p ) )
2 wksv
 |-  { <. f , p >. | f ( Walks ` G ) p } e. _V
3 trliswlk
 |-  ( f ( Trails ` G ) p -> f ( Walks ` G ) p )
4 3 ssopab2i
 |-  { <. f , p >. | f ( Trails ` G ) p } C_ { <. f , p >. | f ( Walks ` G ) p }
5 2 4 ssexi
 |-  { <. f , p >. | f ( Trails ` G ) p } e. _V
6 5 a1i
 |-  ( T. -> { <. f , p >. | f ( Trails ` G ) p } e. _V )
7 df-spths
 |-  SPaths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ Fun `' p ) } )
8 1 6 7 fvmptopab
 |-  ( T. -> ( SPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) } )
9 8 mptru
 |-  ( SPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) }