Metamath Proof Explorer

Theorem 0wlkon

Description: A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 3-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢V=Vtx⁡G
2 simpl ⊢P:0…0⟶V∧P⁡0=N→P:0…0⟶V
3 1 0wlkonlem1 ⊢P:0…0⟶V∧P⁡0=N→N∈V∧N∈V
4 1 1vgrex ⊢N∈V→G∈V
5 4 adantr ⊢N∈V∧N∈V→G∈V
6 1 0wlk ⊢G∈V→∅Walks⁡GP↔P:0…0⟶V
7 3 5 6 3syl ⊢P:0…0⟶V∧P⁡0=N→∅Walks⁡GP↔P:0…0⟶V
8 2 7 mpbird ⊢P:0…0⟶V∧P⁡0=N→∅Walks⁡GP
9 simpr ⊢P:0…0⟶V∧P⁡0=N→P⁡0=N
10 hash0 ⊢∅=0
11 10 fveq2i ⊢P⁡∅=P⁡0
12 11 9 eqtrid ⊢P:0…0⟶V∧P⁡0=N→P⁡∅=N
13 0ex ⊢∅∈V
14 13 a1i ⊢P:0…0⟶V∧P⁡0=N→∅∈V
15 1 0wlkonlem2 ⊢P:0…0⟶V∧P⁡0=N→P∈V↑𝑝𝑚0…0
16 1 iswlkon ⊢N∈V∧N∈V∧∅∈V∧P∈V↑𝑝𝑚0…0→∅NWalksOn⁡GNP↔∅Walks⁡GP∧P⁡0=N∧P⁡∅=N
17 3 14 15 16 syl12anc ⊢P:0…0⟶V∧P⁡0=N→∅NWalksOn⁡GNP↔∅Walks⁡GP∧P⁡0=N∧P⁡∅=N
18 8 9 12 17 mpbir3and ⊢P:0…0⟶V∧P⁡0=N→∅NWalksOn⁡GNP