0spth

Description: A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 18-Jan-2021) (Revised by AV, 30-Oct-2021)

		Ref	Expression
	Hypothesis	0pth.v	$⊢ V = Vtx (G)$
	Assertion	0spth	$⊢ G \in W \to (\emptyset SPaths (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$

Proof

Step	Hyp	Ref	Expression
1		0pth.v	$⊢ V = Vtx (G)$
2	1	0trl	$⊢ G \in W \to (\emptyset Trails (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$
3	2	anbi1d	$⊢ G \in W \to ((\emptyset Trails (G) P \land Fun P^{-1}) \leftrightarrow (P : (0 \dots 0) ⟶ V \land Fun P^{-1}))$
4		isspth	$⊢ \emptyset SPaths (G) P \leftrightarrow (\emptyset Trails (G) P \land Fun P^{-1})$
5		fz0sn	$⊢ (0 \dots 0) = \{0\}$
6	5	feq2i	$⊢ P : (0 \dots 0) ⟶ V \leftrightarrow P : \{0\} ⟶ V$
7		c0ex	$⊢ 0 \in V$
8	7	fsn2	$⊢ P : \{0\} ⟶ V \leftrightarrow (P (0) \in V \land P = \{⟨0, P (0)⟩\})$
9		funcnvsn	$⊢ Fun {\{⟨0, P (0)⟩\}}^{-1}$
10		cnveq	$⊢ P = \{⟨0, P (0)⟩\} \to P^{-1} = {\{⟨0, P (0)⟩\}}^{-1}$
11	10	funeqd	$⊢ P = \{⟨0, P (0)⟩\} \to (Fun P^{-1} \leftrightarrow Fun {\{⟨0, P (0)⟩\}}^{-1})$
12	9 11	mpbiri	$⊢ P = \{⟨0, P (0)⟩\} \to Fun P^{-1}$
13	8 12	simplbiim	$⊢ P : \{0\} ⟶ V \to Fun P^{-1}$
14	6 13	sylbi	$⊢ P : (0 \dots 0) ⟶ V \to Fun P^{-1}$
15	14	pm4.71i	$⊢ P : (0 \dots 0) ⟶ V \leftrightarrow (P : (0 \dots 0) ⟶ V \land Fun P^{-1})$
16	3 4 15	3bitr4g	$⊢ G \in W \to (\emptyset SPaths (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$

Metamath Proof Explorer

Theorem 0spth

Proof