Metamath Proof Explorer

Theorem pthsfval

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

Ref Expression
Assertion pthsfval 
|- ( Paths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) }

Proof

Step Hyp Ref Expression
1 biidd 
 |-  ( ( T. /\ g = G ) -> ( ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) <-> ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) )
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-pths 
 |-  Paths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) } )
8 3anass 
 |-  ( ( f ( Trails ` g ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) <-> ( f ( Trails ` g ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) )
9 8 opabbii 
 |-  { <. f , p >. | ( f ( Trails ` g ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) } = { <. f , p >. | ( f ( Trails ` g ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) }
10 9 mpteq2i 
 |-  ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) } ) = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) } )
11 7 10 eqtri 
 |-  Paths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) } )
12 1 6 11 fvmptopab 
 |-  ( T. -> ( Paths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) } )
13 12 mptru 
 |-  ( Paths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) }
14 3anass 
 |-  ( ( f ( Trails ` G ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) <-> ( f ( Trails ` G ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) )
15 14 bicomi 
 |-  ( ( f ( Trails ` G ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) <-> ( f ( Trails ` G ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) )
16 15 opabbii 
 |-  { <. f , p >. | ( f ( Trails ` G ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) } = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) }
17 13 16 eqtri 
 |-  ( Paths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) }