Metamath Proof Explorer

Theorem 0pthon

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) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0pthon.v ⊢V=Vtx⁡G
Assertion 0pthon ⊢P:0…0⟶V∧P⁡0=N→∅NPathsOn⁡GNP

Proof

Step Hyp Ref Expression
1 0pthon.v ⊢V=Vtx⁡G
2 1 0trlon ⊢P:0…0⟶V∧P⁡0=N→∅NTrailsOn⁡GNP
3 simpl ⊢P:0…0⟶V∧P⁡0=N→P:0…0⟶V
4 id ⊢P:0…0⟶V→P:0…0⟶V
5 0z ⊢0∈ℤ
6 elfz3 ⊢0∈ℤ→0∈0…0
7 5 6 mp1i ⊢P:0…0⟶V→0∈0…0
8 4 7 ffvelcdmd ⊢P:0…0⟶V→P⁡0∈V
9 8 adantr ⊢P:0…0⟶V∧P⁡0=N→P⁡0∈V
10 eleq1 ⊢P⁡0=N→P⁡0∈V↔N∈V
11 10 adantl ⊢P:0…0⟶V∧P⁡0=N→P⁡0∈V↔N∈V
12 9 11 mpbid ⊢P:0…0⟶V∧P⁡0=N→N∈V
13 1 1vgrex ⊢N∈V→G∈V
14 1 0pth ⊢G∈V→∅Paths⁡GP↔P:0…0⟶V
15 12 13 14 3syl ⊢P:0…0⟶V∧P⁡0=N→∅Paths⁡GP↔P:0…0⟶V
16 3 15 mpbird ⊢P:0…0⟶V∧P⁡0=N→∅Paths⁡GP
17 1 0wlkonlem1 ⊢P:0…0⟶V∧P⁡0=N→N∈V∧N∈V
18 1 0wlkonlem2 ⊢P:0…0⟶V∧P⁡0=N→P∈V↑𝑝𝑚0…0
19 0ex ⊢∅∈V
20 18 19 jctil ⊢P:0…0⟶V∧P⁡0=N→∅∈V∧P∈V↑𝑝𝑚0…0
21 1 ispthson ⊢N∈V∧N∈V∧∅∈V∧P∈V↑𝑝𝑚0…0→∅NPathsOn⁡GNP↔∅NTrailsOn⁡GNP∧∅Paths⁡GP
22 17 20 21 syl2anc ⊢P:0…0⟶V∧P⁡0=N→∅NPathsOn⁡GNP↔∅NTrailsOn⁡GNP∧∅Paths⁡GP
23 2 16 22 mpbir2and ⊢P:0…0⟶V∧P⁡0=N→∅NPathsOn⁡GNP