Metamath Proof Explorer

Theorem 0spth

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

Ref Expression
Hypothesis 0pth.v ⊢ V = Vtx ⁡ G
Assertion 0spth ⊢ G ∈ W → ∅ SPaths ⁡ G P ↔ P : 0 … 0 ⟶ V

Proof

Step Hyp Ref Expression
1 0pth.v ⊢ V = Vtx ⁡ G
2 1 0trl ⊢ G ∈ W → ∅ Trails ⁡ G P ↔ P : 0 … 0 ⟶ V
3 2 anbi1d ⊢ G ∈ W → ∅ Trails ⁡ G P ∧ Fun ⁡ P -1 ↔ P : 0 … 0 ⟶ V ∧ Fun ⁡ P -1
4 isspth ⊢ ∅ SPaths ⁡ G P ↔ ∅ Trails ⁡ G P ∧ Fun ⁡ P -1
5 fz0sn ⊢ 0 … 0 = 0
6 5 feq2i ⊢ P : 0 … 0 ⟶ V ↔ P : 0 ⟶ V
7 c0ex ⊢ 0 ∈ V
8 7 fsn2 ⊢ P : 0 ⟶ V ↔ P ⁡ 0 ∈ V ∧ P = 0 P ⁡ 0
9 funcnvsn ⊢ Fun ⁡ 0 P ⁡ 0 -1
10 cnveq ⊢ P = 0 P ⁡ 0 → P -1 = 0 P ⁡ 0 -1
11 10 funeqd ⊢ P = 0 P ⁡ 0 → Fun ⁡ P -1 ↔ Fun ⁡ 0 P ⁡ 0 -1
12 9 11 mpbiri ⊢ P = 0 P ⁡ 0 → Fun ⁡ P -1
13 8 12 simplbiim ⊢ P : 0 ⟶ V → Fun ⁡ P -1
14 6 13 sylbi ⊢ P : 0 … 0 ⟶ V → Fun ⁡ P -1
15 14 pm4.71i ⊢ P : 0 … 0 ⟶ V ↔ P : 0 … 0 ⟶ V ∧ Fun ⁡ P -1
16 3 4 15 3bitr4g ⊢ G ∈ W → ∅ SPaths ⁡ G P ↔ P : 0 … 0 ⟶ V