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 (G) = \emptyset \to Walks (G) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$⊢ Walks (G) = \emptyset \to (Vtx (G) = \emptyset \to Walks (G) = \emptyset)$
2		neq0	$⊢ \neg Walks (G) = \emptyset \leftrightarrow \exists w w \in Walks (G)$
3		wlkv0	$⊢ (Vtx (G) = \emptyset \land w \in Walks (G)) \to (1^{st} (w) = \emptyset \land 2^{nd} (w) = \emptyset)$
4		wlkcpr	$⊢ w \in Walks (G) \leftrightarrow 1^{st} (w) Walks (G) 2^{nd} (w)$
5		wlkn0	$⊢ 1^{st} (w) Walks (G) 2^{nd} (w) \to 2^{nd} (w) \neq \emptyset$
6		eqneqall	$⊢ 2^{nd} (w) = \emptyset \to (2^{nd} (w) \neq \emptyset \to Walks (G) = \emptyset)$
7	6	adantl	$⊢ (1^{st} (w) = \emptyset \land 2^{nd} (w) = \emptyset) \to (2^{nd} (w) \neq \emptyset \to Walks (G) = \emptyset)$
8	5 7	syl5com	$⊢ 1^{st} (w) Walks (G) 2^{nd} (w) \to ((1^{st} (w) = \emptyset \land 2^{nd} (w) = \emptyset) \to Walks (G) = \emptyset)$
9	4 8	sylbi	$⊢ w \in Walks (G) \to ((1^{st} (w) = \emptyset \land 2^{nd} (w) = \emptyset) \to Walks (G) = \emptyset)$
10	9	adantl	$⊢ (Vtx (G) = \emptyset \land w \in Walks (G)) \to ((1^{st} (w) = \emptyset \land 2^{nd} (w) = \emptyset) \to Walks (G) = \emptyset)$
11	3 10	mpd	$⊢ (Vtx (G) = \emptyset \land w \in Walks (G)) \to Walks (G) = \emptyset$
12	11	expcom	$⊢ w \in Walks (G) \to (Vtx (G) = \emptyset \to Walks (G) = \emptyset)$
13	12	exlimiv	$⊢ \exists w w \in Walks (G) \to (Vtx (G) = \emptyset \to Walks (G) = \emptyset)$
14	2 13	sylbi	$⊢ \neg Walks (G) = \emptyset \to (Vtx (G) = \emptyset \to Walks (G) = \emptyset)$
15	1 14	pm2.61i	$⊢ Vtx (G) = \emptyset \to Walks (G) = \emptyset$