Step |
Hyp |
Ref |
Expression |
1 |
|
biidd |
|- ( 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 |
|
df-pths |
|- Paths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) } ) |
3 |
|
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 ) ) ) ) = (/) ) ) ) |
4 |
3
|
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 ) ) ) ) = (/) ) ) } |
5 |
4
|
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 ) ) ) ) = (/) ) ) } ) |
6 |
2 5
|
eqtri |
|- Paths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ ( Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) ) } ) |
7 |
1 6
|
fvmptopab |
|- ( Paths ` G ) = { <. 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 |
7 9
|
eqtr4i |
|- ( Paths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) } |