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

Proof

Step Hyp Ref Expression
1 0pthon.v ⊢ V = Vtx ⁡ G
2 1 0trlon ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ N TrailsOn ⁡ G N P
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 ⁡ G P ↔ P : 0 … 0 ⟶ V
15 12 13 14 3syl ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ Paths ⁡ G P ↔ P : 0 … 0 ⟶ V
16 3 15 mpbird ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ Paths ⁡ G P
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 → ∅ N PathsOn ⁡ G N P ↔ ∅ N TrailsOn ⁡ G N P ∧ ∅ Paths ⁡ G P
22 17 20 21 syl2anc ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ N PathsOn ⁡ G N P ↔ ∅ N TrailsOn ⁡ G N P ∧ ∅ Paths ⁡ G P
23 2 16 22 mpbir2and ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → ∅ N PathsOn ⁡ G N P