Theorem 0pthon1

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)

	Ref	Expression
Hypothesis	0pthon.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	0pthon1	⊢ ( 𝑁 ∈ 𝑉 → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		0pthon.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eqidd	⊢ ( 𝑁 ∈ 𝑉 → { ⟨ 0 , 𝑁 ⟩ } = { ⟨ 0 , 𝑁 ⟩ } )
3		1fv	⊢ ( ( 𝑁 ∈ 𝑉 ∧ { ⟨ 0 , 𝑁 ⟩ } = { ⟨ 0 , 𝑁 ⟩ } ) → ( { ⟨ 0 , 𝑁 ⟩ } : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) )
4	2 3	mpdan	⊢ ( 𝑁 ∈ 𝑉 → ( { ⟨ 0 , 𝑁 ⟩ } : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) )
5	1	0pthon	⊢ ( ( { ⟨ 0 , 𝑁 ⟩ } : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } )
6	4 5	syl	⊢ ( 𝑁 ∈ 𝑉 → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { ⟨ 0 , 𝑁 ⟩ } )