Metamath Proof Explorer

Theorem 0pth

Description: A pair of an empty set (of edges) and a second set (of vertices) is a path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 19-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0pth.v 
|- V = ( Vtx ` G )
Assertion 0pth 
|- ( G e. W -> ( (/) ( Paths ` G ) P <-> P : ( 0 ... 0 ) --> V ) )

Proof

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 ) )