Theorem wlk0prc

Description: There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

	Ref	Expression
Assertion	wlk0prc	⊢ ( ( 𝑆 ∉ V ∧ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝐺 ) ) → ( Walks ‘ 𝐺 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝐺 ) ↔ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝑆 ) )
2	1	biimpi	⊢ ( ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝐺 ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝑆 ) )
3		vtxvalprc	⊢ ( 𝑆 ∉ V → ( Vtx ‘ 𝑆 ) = ∅ )
4	2 3	sylan9eqr	⊢ ( ( 𝑆 ∉ V ∧ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝐺 ) ) → ( Vtx ‘ 𝐺 ) = ∅ )
5		g0wlk0	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ )
6	4 5	syl	⊢ ( ( 𝑆 ∉ V ∧ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝐺 ) ) → ( Walks ‘ 𝐺 ) = ∅ )