Step |
Hyp |
Ref |
Expression |
1 |
|
0pth.v |
|- V = ( Vtx ` G ) |
2 |
|
ispth |
|- ( (/) ( Paths ` G ) P <-> ( (/) ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) ) |
3 |
2
|
a1i |
|- ( G e. W -> ( (/) ( Paths ` G ) P <-> ( (/) ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) ) ) |
4 |
|
3anass |
|- ( ( (/) ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) <-> ( (/) ( Trails ` G ) P /\ ( Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) ) ) |
5 |
4
|
a1i |
|- ( G e. W -> ( ( (/) ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) <-> ( (/) ( Trails ` G ) P /\ ( Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) ) ) ) |
6 |
|
funcnv0 |
|- Fun `' (/) |
7 |
|
hash0 |
|- ( # ` (/) ) = 0 |
8 |
|
0le1 |
|- 0 <_ 1 |
9 |
7 8
|
eqbrtri |
|- ( # ` (/) ) <_ 1 |
10 |
|
1z |
|- 1 e. ZZ |
11 |
|
0z |
|- 0 e. ZZ |
12 |
7 11
|
eqeltri |
|- ( # ` (/) ) e. ZZ |
13 |
|
fzon |
|- ( ( 1 e. ZZ /\ ( # ` (/) ) e. ZZ ) -> ( ( # ` (/) ) <_ 1 <-> ( 1 ..^ ( # ` (/) ) ) = (/) ) ) |
14 |
10 12 13
|
mp2an |
|- ( ( # ` (/) ) <_ 1 <-> ( 1 ..^ ( # ` (/) ) ) = (/) ) |
15 |
9 14
|
mpbi |
|- ( 1 ..^ ( # ` (/) ) ) = (/) |
16 |
15
|
reseq2i |
|- ( P |` ( 1 ..^ ( # ` (/) ) ) ) = ( P |` (/) ) |
17 |
|
res0 |
|- ( P |` (/) ) = (/) |
18 |
16 17
|
eqtri |
|- ( P |` ( 1 ..^ ( # ` (/) ) ) ) = (/) |
19 |
18
|
cnveqi |
|- `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) = `' (/) |
20 |
19
|
funeqi |
|- ( Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) <-> Fun `' (/) ) |
21 |
6 20
|
mpbir |
|- Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) |
22 |
15
|
imaeq2i |
|- ( P " ( 1 ..^ ( # ` (/) ) ) ) = ( P " (/) ) |
23 |
|
ima0 |
|- ( P " (/) ) = (/) |
24 |
22 23
|
eqtri |
|- ( P " ( 1 ..^ ( # ` (/) ) ) ) = (/) |
25 |
24
|
ineq2i |
|- ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = ( ( P " { 0 , ( # ` (/) ) } ) i^i (/) ) |
26 |
|
in0 |
|- ( ( P " { 0 , ( # ` (/) ) } ) i^i (/) ) = (/) |
27 |
25 26
|
eqtri |
|- ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) |
28 |
21 27
|
pm3.2i |
|- ( Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) |
29 |
28
|
biantru |
|- ( (/) ( Trails ` G ) P <-> ( (/) ( Trails ` G ) P /\ ( Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) ) ) |
30 |
5 29
|
bitr4di |
|- ( G e. W -> ( ( (/) ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` (/) ) ) ) /\ ( ( P " { 0 , ( # ` (/) ) } ) i^i ( P " ( 1 ..^ ( # ` (/) ) ) ) ) = (/) ) <-> (/) ( Trails ` G ) P ) ) |
31 |
1
|
0trl |
|- ( G e. W -> ( (/) ( Trails ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |
32 |
3 30 31
|
3bitrd |
|- ( G e. W -> ( (/) ( Paths ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |