Metamath Proof Explorer

Theorem 0trlon

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

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

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ V = Vtx ⁡ G
2 1 0wlkon ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ N WalksOn ⁡ G N P
3 simpl ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → P : 0 … 0 ⟶ V
4 1 0wlkonlem1 ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → N ∈ V ∧ N ∈ V
5 1 1vgrex ⊢ N ∈ V → G ∈ V
6 5 adantr ⊢ N ∈ V ∧ N ∈ V → G ∈ V
7 1 0trl ⊢ G ∈ V → ∅ Trails ⁡ G P ↔ P : 0 … 0 ⟶ V
8 4 6 7 3syl ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ Trails ⁡ G P ↔ P : 0 … 0 ⟶ V
9 3 8 mpbird ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ Trails ⁡ G P
10 0ex ⊢ ∅ ∈ V
11 10 a1i ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ ∈ V
12 1 0wlkonlem2 ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → P ∈ V ↑ 𝑝𝑚 0 … 0
13 1 istrlson ⊢ N ∈ V ∧ N ∈ V ∧ ∅ ∈ V ∧ P ∈ V ↑ 𝑝𝑚 0 … 0 → ∅ N TrailsOn ⁡ G N P ↔ ∅ N WalksOn ⁡ G N P ∧ ∅ Trails ⁡ G P
14 4 11 12 13 syl12anc ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ N TrailsOn ⁡ G N P ↔ ∅ N WalksOn ⁡ G N P ∧ ∅ Trails ⁡ G P
15 2 9 14 mpbir2and ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ N TrailsOn ⁡ G N P