This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion 0pthon ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 0pthon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 0trlon ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 )
3 simpl ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 )
4 id ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 )
5 0z ⊢ 0 ∈ ℤ
6 elfz3 ⊢ ( 0 ∈ ℤ → 0 ∈ ( 0 ... 0 ) )
7 5 6 mp1i ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → 0 ∈ ( 0 ... 0 ) )
8 4 7 ffvelcdmd ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
9 8 adantr ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
10 eleq1 ⊢ ( ( 𝑃 ‘ 0 ) = 𝑁 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ↔ 𝑁 ∈ 𝑉 ) )
11 10 adantl ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ↔ 𝑁 ∈ 𝑉 ) )
12 9 11 mpbid ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑁 ∈ 𝑉 )
13 1 1vgrex ⊢ ( 𝑁 ∈ 𝑉 → 𝐺 ∈ V )
14 1 0pth ⊢ ( 𝐺 ∈ V → ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
15 12 13 14 3syl ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
16 3 15 mpbird ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( Paths ‘ 𝐺 ) 𝑃 )
17 1 0wlkonlem1 ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )
18 1 0wlkonlem2 ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) )
19 0ex ⊢ ∅ ∈ V
20 18 19 jctil ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ∅ ∈ V ∧ 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) )
21 1 ispthson ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( ∅ ∈ V ∧ 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) ) → ( ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ↔ ( ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ∧ ∅ ( Paths ‘ 𝐺 ) 𝑃 ) ) )
22 17 20 21 syl2anc ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ↔ ( ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ∧ ∅ ( Paths ‘ 𝐺 ) 𝑃 ) ) )
23 2 16 22 mpbir2and ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑃 )