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 ffvelrnd ( 𝑃 : ( 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 ‘ 𝐺 ) 𝑁 ) 𝑃 )