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 → ∅ N WalksOn ⁡ G N P

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 ⁡ G P ↔ P : 0 … 0 ⟶ V
7 3 5 6 3syl ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ Walks ⁡ G P ↔ P : 0 … 0 ⟶ V
8 2 7 mpbird ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ Walks ⁡ G P
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 → ∅ N WalksOn ⁡ G N P ↔ ∅ Walks ⁡ G P ∧ P ⁡ 0 = N ∧ P ⁡ ∅ = N
17 3 14 15 16 syl12anc ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ N WalksOn ⁡ G N P ↔ ∅ Walks ⁡ G P ∧ P ⁡ 0 = N ∧ P ⁡ ∅ = N
18 8 9 12 17 mpbir3and ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ N WalksOn ⁡ G N P