Metamath Proof Explorer


Theorem 0pthon1

Description: A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 20-Jan-2021)

Ref Expression
Hypothesis 0pthon.v V = Vtx G
Assertion 0pthon1 N V N PathsOn G N 0 N

Proof

Step Hyp Ref Expression
1 0pthon.v V = Vtx G
2 eqidd N V 0 N = 0 N
3 1fv N V 0 N = 0 N 0 N : 0 0 V 0 N 0 = N
4 2 3 mpdan N V 0 N : 0 0 V 0 N 0 = N
5 1 0pthon 0 N : 0 0 V 0 N 0 = N N PathsOn G N 0 N
6 4 5 syl N V N PathsOn G N 0 N