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