This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0pthonv

Description: For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 21-Jan-2021)

Ref Expression
Hypothesis 0pthon.v ⊢ V = Vtx ⁡ G
Assertion 0pthonv ⊢ N ∈ V → ∃ f ∃ p f N PathsOn ⁡ G N p

Proof

Step Hyp Ref Expression
1 0pthon.v ⊢ V = Vtx ⁡ G
2 0ex ⊢ ∅ ∈ V
3 snex ⊢ 0 N ∈ V
4 2 3 pm3.2i ⊢ ∅ ∈ V ∧ 0 N ∈ V
5 1 0pthon1 ⊢ N ∈ V → ∅ N PathsOn ⁡ G N 0 N
6 breq12 ⊢ f = ∅ ∧ p = 0 N → f N PathsOn ⁡ G N p ↔ ∅ N PathsOn ⁡ G N 0 N
7 6 spc2egv ⊢ ∅ ∈ V ∧ 0 N ∈ V → ∅ N PathsOn ⁡ G N 0 N → ∃ f ∃ p f N PathsOn ⁡ G N p
8 4 5 7 mpsyl ⊢ N ∈ V → ∃ f ∃ p f N PathsOn ⁡ G N p