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=VtxG
Assertion 0pth GWPathsGPP:00V

Proof

Step Hyp Ref Expression
1 0pth.v V=VtxG
2 ispth PathsGPTrailsGPFunP1..^-1P0P1..^=
3 2 a1i GWPathsGPTrailsGPFunP1..^-1P0P1..^=
4 3anass TrailsGPFunP1..^-1P0P1..^=TrailsGPFunP1..^-1P0P1..^=
5 4 a1i GWTrailsGPFunP1..^-1P0P1..^=TrailsGPFunP1..^-1P0P1..^=
6 funcnv0 Fun-1
7 hash0 =0
8 0le1 01
9 7 8 eqbrtri 1
10 1z 1
11 0z 0
12 7 11 eqeltri
13 fzon 111..^=
14 10 12 13 mp2an 11..^=
15 9 14 mpbi 1..^=
16 15 reseq2i P1..^=P
17 res0 P=
18 16 17 eqtri P1..^=
19 18 cnveqi P1..^-1=-1
20 19 funeqi FunP1..^-1Fun-1
21 6 20 mpbir FunP1..^-1
22 15 imaeq2i P1..^=P
23 ima0 P=
24 22 23 eqtri P1..^=
25 24 ineq2i P0P1..^=P0
26 in0 P0=
27 25 26 eqtri P0P1..^=
28 21 27 pm3.2i FunP1..^-1P0P1..^=
29 28 biantru TrailsGPTrailsGPFunP1..^-1P0P1..^=
30 5 29 bitr4di GWTrailsGPFunP1..^-1P0P1..^=TrailsGP
31 1 0trl GWTrailsGPP:00V
32 3 30 31 3bitrd GWPathsGPP:00V