Metamath Proof Explorer

Theorem 0clwlkv

Description: Any vertex (more precisely, a pair of an empty set (of edges) and a singleton function to this vertex) determines a closed walk of length 0. (Contributed by AV, 11-Feb-2022)

		Ref	Expression
	Hypothesis	0clwlk.v	$⊢ V = Vtx (G)$
	Assertion	0clwlkv	$⊢ (X \in V \land F = \emptyset \land P : \{0\} ⟶ \{X\}) \to F ClWalks (G) P$

Proof

Step	Hyp	Ref	Expression
1		0clwlk.v	$⊢ V = Vtx (G)$
2		fz0sn	$⊢ (0 \dots 0) = \{0\}$
3	2	eqcomi	$⊢ \{0\} = (0 \dots 0)$
4	3	feq2i	$⊢ P : \{0\} ⟶ \{X\} \leftrightarrow P : (0 \dots 0) ⟶ \{X\}$
5	4	biimpi	$⊢ P : \{0\} ⟶ \{X\} \to P : (0 \dots 0) ⟶ \{X\}$
6	5	3ad2ant3	$⊢ (X \in V \land F = \emptyset \land P : \{0\} ⟶ \{X\}) \to P : (0 \dots 0) ⟶ \{X\}$
7		snssi	$⊢ X \in V \to \{X\} \subseteq V$
8	7	3ad2ant1	$⊢ (X \in V \land F = \emptyset \land P : \{0\} ⟶ \{X\}) \to \{X\} \subseteq V$
9	6 8	fssd	$⊢ (X \in V \land F = \emptyset \land P : \{0\} ⟶ \{X\}) \to P : (0 \dots 0) ⟶ V$
10		breq1	$⊢ F = \emptyset \to (F ClWalks (G) P \leftrightarrow \emptyset ClWalks (G) P)$
11	10	3ad2ant2	$⊢ (X \in V \land F = \emptyset \land P : \{0\} ⟶ \{X\}) \to (F ClWalks (G) P \leftrightarrow \emptyset ClWalks (G) P)$
12	1	1vgrex	$⊢ X \in V \to G \in V$
13	1	0clwlk	$⊢ G \in V \to (\emptyset ClWalks (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$
14	12 13	syl	$⊢ X \in V \to (\emptyset ClWalks (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$
15	14	3ad2ant1	$⊢ (X \in V \land F = \emptyset \land P : \{0\} ⟶ \{X\}) \to (\emptyset ClWalks (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$
16	11 15	bitrd	$⊢ (X \in V \land F = \emptyset \land P : \{0\} ⟶ \{X\}) \to (F ClWalks (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$
17	9 16	mpbird	$⊢ (X \in V \land F = \emptyset \land P : \{0\} ⟶ \{X\}) \to F ClWalks (G) P$