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 ⁡ 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 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅
3 2 a1i ⊢ G ∈ W → ∅ Paths ⁡ G P ↔ ∅ Trails ⁡ G P ∧ Fun ⁡ P ↾ 1 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅
4 3anass ⊢ ∅ Trails ⁡ G P ∧ Fun ⁡ P ↾ 1 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅ ↔ ∅ Trails ⁡ G P ∧ Fun ⁡ P ↾ 1 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅
5 4 a1i ⊢ G ∈ W → ∅ Trails ⁡ G P ∧ Fun ⁡ P ↾ 1 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅ ↔ ∅ Trails ⁡ G P ∧ Fun ⁡ P ↾ 1 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅
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 ⊢ P 1 ..^ ∅ = P ∅
23 ima0 ⊢ P ∅ = ∅
24 22 23 eqtri ⊢ P 1 ..^ ∅ = ∅
25 24 ineq2i ⊢ P 0 ∅ ∩ P 1 ..^ ∅ = P 0 ∅ ∩ ∅
26 in0 ⊢ P 0 ∅ ∩ ∅ = ∅
27 25 26 eqtri ⊢ P 0 ∅ ∩ P 1 ..^ ∅ = ∅
28 21 27 pm3.2i ⊢ Fun ⁡ P ↾ 1 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅
29 28 biantru ⊢ ∅ Trails ⁡ G P ↔ ∅ Trails ⁡ G P ∧ Fun ⁡ P ↾ 1 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅
30 5 29 bitr4di ⊢ G ∈ W → ∅ Trails ⁡ G P ∧ Fun ⁡ P ↾ 1 ..^ ∅ -1 ∧ P 0 ∅ ∩ P 1 ..^ ∅ = ∅ ↔ ∅ Trails ⁡ G P
31 1 0trl ⊢ G ∈ W → ∅ Trails ⁡ G P ↔ P : 0 … 0 ⟶ V
32 3 30 31 3bitrd ⊢ G ∈ W → ∅ Paths ⁡ G P ↔ P : 0 … 0 ⟶ V