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∈W→∅Paths⁡GP↔P:0…0⟶V

Proof

Step Hyp Ref Expression
1 0pth.v ⊢V=Vtx⁡G
2 ispth ⊢∅Paths⁡GP↔∅Trails⁡GP∧Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅
3 2 a1i ⊢G∈W→∅Paths⁡GP↔∅Trails⁡GP∧Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅
4 3anass ⊢∅Trails⁡GP∧Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅↔∅Trails⁡GP∧Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅
5 4 a1i ⊢G∈W→∅Trails⁡GP∧Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅↔∅Trails⁡GP∧Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅
6 funcnv0 ⊢Fun⁡∅-1
7 hash0 ⊢∅=0
8 0le1 ⊢0≤1
9 7 8 eqbrtri ⊢∅≤1
10 1z ⊢1∈ℤ
11 0z ⊢0∈ℤ
12 7 11 eqeltri ⊢∅∈ℤ
13 fzon ⊢1∈ℤ∧∅∈ℤ→∅≤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..^∅-1=∅-1
20 19 funeqi ⊢Fun⁡P↾1..^∅-1↔Fun⁡∅-1
21 6 20 mpbir ⊢Fun⁡P↾1..^∅-1
22 15 imaeq2i ⊢P1..^∅=P∅
23 ima0 ⊢P∅=∅
24 22 23 eqtri ⊢P1..^∅=∅
25 24 ineq2i ⊢P0∅∩P1..^∅=P0∅∩∅
26 in0 ⊢P0∅∩∅=∅
27 25 26 eqtri ⊢P0∅∩P1..^∅=∅
28 21 27 pm3.2i ⊢Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅
29 28 biantru ⊢∅Trails⁡GP↔∅Trails⁡GP∧Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅
30 5 29 bitr4di ⊢G∈W→∅Trails⁡GP∧Fun⁡P↾1..^∅-1∧P0∅∩P1..^∅=∅↔∅Trails⁡GP
31 1 0trl ⊢G∈W→∅Trails⁡GP↔P:0…0⟶V
32 3 30 31 3bitrd ⊢G∈W→∅Paths⁡GP↔P:0…0⟶V