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

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

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 0wlkon ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑁 ) 𝑃 )
3 simpl ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 )
4 1 0wlkonlem1 ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )
5 1 1vgrex ⊢ ( 𝑁 ∈ 𝑉 → 𝐺 ∈ V )
6 5 adantr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → 𝐺 ∈ V )
7 1 0trl ⊢ ( 𝐺 ∈ V → ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
8 4 6 7 3syl ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
9 3 8 mpbird ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( Trails ‘ 𝐺 ) 𝑃 )
10 0ex ⊢ ∅ ∈ V
11 10 a1i ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ∈ V )
12 1 0wlkonlem2 ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) )
13 1 istrlson ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( ∅ ∈ V ∧ 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) ) → ( ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ↔ ( ∅ ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑁 ) 𝑃 ∧ ∅ ( Trails ‘ 𝐺 ) 𝑃 ) ) )
14 4 11 12 13 syl12anc ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ↔ ( ∅ ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑁 ) 𝑃 ∧ ∅ ( Trails ‘ 𝐺 ) 𝑃 ) ) )
15 2 9 14 mpbir2and ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 )