wlkv0

Description: If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

		Ref	Expression
	Assertion	wlkv0	$⊢ (Vtx (G) = \emptyset \land W \in Walks (G)) \to (1^{st} (W) = \emptyset \land 2^{nd} (W) = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		wlkcpr	$⊢ W \in Walks (G) \leftrightarrow 1^{st} (W) Walks (G) 2^{nd} (W)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3	2	wlkf	$⊢ 1^{st} (W) Walks (G) 2^{nd} (W) \to 1^{st} (W) \in Word dom iEdg (G)$
4		eqid	$⊢ Vtx (G) = Vtx (G)$
5	4	wlkp	$⊢ 1^{st} (W) Walks (G) 2^{nd} (W) \to 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G)$
6	3 5	jca	$⊢ 1^{st} (W) Walks (G) 2^{nd} (W) \to (1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G))$
7		feq3	$⊢ Vtx (G) = \emptyset \to (2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G) \leftrightarrow 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ \emptyset)$
8		f00	$⊢ 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ \emptyset \leftrightarrow (2^{nd} (W) = \emptyset \land (0 \dots \|1^{st} (W)\|) = \emptyset)$
9	7 8	bitrdi	$⊢ Vtx (G) = \emptyset \to (2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G) \leftrightarrow (2^{nd} (W) = \emptyset \land (0 \dots \|1^{st} (W)\|) = \emptyset))$
10		0z	$⊢ 0 \in ℤ$
11		nn0z	$⊢ \|1^{st} (W)\| \in ℕ_{0} \to \|1^{st} (W)\| \in ℤ$
12		fzn	$⊢ (0 \in ℤ \land \|1^{st} (W)\| \in ℤ) \to (\|1^{st} (W)\| < 0 \leftrightarrow (0 \dots \|1^{st} (W)\|) = \emptyset)$
13	10 11 12	sylancr	$⊢ \|1^{st} (W)\| \in ℕ_{0} \to (\|1^{st} (W)\| < 0 \leftrightarrow (0 \dots \|1^{st} (W)\|) = \emptyset)$
14		nn0nlt0	$⊢ \|1^{st} (W)\| \in ℕ_{0} \to \neg \|1^{st} (W)\| < 0$
15	14	pm2.21d	$⊢ \|1^{st} (W)\| \in ℕ_{0} \to (\|1^{st} (W)\| < 0 \to 1^{st} (W) = \emptyset)$
16	13 15	sylbird	$⊢ \|1^{st} (W)\| \in ℕ_{0} \to ((0 \dots \|1^{st} (W)\|) = \emptyset \to 1^{st} (W) = \emptyset)$
17	16	com12	$⊢ (0 \dots \|1^{st} (W)\|) = \emptyset \to (\|1^{st} (W)\| \in ℕ_{0} \to 1^{st} (W) = \emptyset)$
18	17	adantl	$⊢ (2^{nd} (W) = \emptyset \land (0 \dots \|1^{st} (W)\|) = \emptyset) \to (\|1^{st} (W)\| \in ℕ_{0} \to 1^{st} (W) = \emptyset)$
19		lencl	$⊢ 1^{st} (W) \in Word dom iEdg (G) \to \|1^{st} (W)\| \in ℕ_{0}$
20	18 19	impel	$⊢ ((2^{nd} (W) = \emptyset \land (0 \dots \|1^{st} (W)\|) = \emptyset) \land 1^{st} (W) \in Word dom iEdg (G)) \to 1^{st} (W) = \emptyset$
21		simpll	$⊢ ((2^{nd} (W) = \emptyset \land (0 \dots \|1^{st} (W)\|) = \emptyset) \land 1^{st} (W) \in Word dom iEdg (G)) \to 2^{nd} (W) = \emptyset$
22	20 21	jca	$⊢ ((2^{nd} (W) = \emptyset \land (0 \dots \|1^{st} (W)\|) = \emptyset) \land 1^{st} (W) \in Word dom iEdg (G)) \to (1^{st} (W) = \emptyset \land 2^{nd} (W) = \emptyset)$
23	22	ex	$⊢ (2^{nd} (W) = \emptyset \land (0 \dots \|1^{st} (W)\|) = \emptyset) \to (1^{st} (W) \in Word dom iEdg (G) \to (1^{st} (W) = \emptyset \land 2^{nd} (W) = \emptyset))$
24	9 23	biimtrdi	$⊢ Vtx (G) = \emptyset \to (2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G) \to (1^{st} (W) \in Word dom iEdg (G) \to (1^{st} (W) = \emptyset \land 2^{nd} (W) = \emptyset)))$
25	24	impcomd	$⊢ Vtx (G) = \emptyset \to ((1^{st} (W) \in Word dom iEdg (G) \land 2^{nd} (W) : (0 \dots \|1^{st} (W)\|) ⟶ Vtx (G)) \to (1^{st} (W) = \emptyset \land 2^{nd} (W) = \emptyset))$
26	6 25	syl5	$⊢ Vtx (G) = \emptyset \to (1^{st} (W) Walks (G) 2^{nd} (W) \to (1^{st} (W) = \emptyset \land 2^{nd} (W) = \emptyset))$
27	1 26	biimtrid	$⊢ Vtx (G) = \emptyset \to (W \in Walks (G) \to (1^{st} (W) = \emptyset \land 2^{nd} (W) = \emptyset))$
28	27	imp	$⊢ (Vtx (G) = \emptyset \land W \in Walks (G)) \to (1^{st} (W) = \emptyset \land 2^{nd} (W) = \emptyset)$

Metamath Proof Explorer

Theorem wlkv0

Proof