Metamath Proof Explorer

Theorem g0wlk0

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	g0wlk0	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ax-1	⊢ ( ( Walks ‘ 𝐺 ) = ∅ → ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ ) )
2		neq0	⊢ ( ¬ ( Walks ‘ 𝐺 ) = ∅ ↔ ∃ 𝑤 𝑤 ∈ ( Walks ‘ 𝐺 ) )
3		wlkv0	⊢ ( ( ( Vtx ‘ 𝐺 ) = ∅ ∧ 𝑤 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝑤 ) = ∅ ∧ ( 2^nd ‘ 𝑤 ) = ∅ ) )
4		wlkcpr	⊢ ( 𝑤 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑤 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) )
5		wlkn0	⊢ ( ( 1^st ‘ 𝑤 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) → ( 2^nd ‘ 𝑤 ) ≠ ∅ )
6		eqneqall	⊢ ( ( 2^nd ‘ 𝑤 ) = ∅ → ( ( 2^nd ‘ 𝑤 ) ≠ ∅ → ( Walks ‘ 𝐺 ) = ∅ ) )
7	6	adantl	⊢ ( ( ( 1^st ‘ 𝑤 ) = ∅ ∧ ( 2^nd ‘ 𝑤 ) = ∅ ) → ( ( 2^nd ‘ 𝑤 ) ≠ ∅ → ( Walks ‘ 𝐺 ) = ∅ ) )
8	5 7	syl5com	⊢ ( ( 1^st ‘ 𝑤 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) → ( ( ( 1^st ‘ 𝑤 ) = ∅ ∧ ( 2^nd ‘ 𝑤 ) = ∅ ) → ( Walks ‘ 𝐺 ) = ∅ ) )
9	4 8	sylbi	⊢ ( 𝑤 ∈ ( Walks ‘ 𝐺 ) → ( ( ( 1^st ‘ 𝑤 ) = ∅ ∧ ( 2^nd ‘ 𝑤 ) = ∅ ) → ( Walks ‘ 𝐺 ) = ∅ ) )
10	9	adantl	⊢ ( ( ( Vtx ‘ 𝐺 ) = ∅ ∧ 𝑤 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ( 1^st ‘ 𝑤 ) = ∅ ∧ ( 2^nd ‘ 𝑤 ) = ∅ ) → ( Walks ‘ 𝐺 ) = ∅ ) )
11	3 10	mpd	⊢ ( ( ( Vtx ‘ 𝐺 ) = ∅ ∧ 𝑤 ∈ ( Walks ‘ 𝐺 ) ) → ( Walks ‘ 𝐺 ) = ∅ )
12	11	expcom	⊢ ( 𝑤 ∈ ( Walks ‘ 𝐺 ) → ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ ) )
13	12	exlimiv	⊢ ( ∃ 𝑤 𝑤 ∈ ( Walks ‘ 𝐺 ) → ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ ) )
14	2 13	sylbi	⊢ ( ¬ ( Walks ‘ 𝐺 ) = ∅ → ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ ) )
15	1 14	pm2.61i	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ )