Metamath Proof Explorer

Theorem 0trlon

Description: A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 8-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Hypothesis	0wlk.v	$⊢ V = Vtx (G)$
	Assertion	0trlon	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to \emptyset (N TrailsOn (G) N) P$

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	$⊢ V = Vtx (G)$
2	1	0wlkon	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to \emptyset (N WalksOn (G) N) P$
3		simpl	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to P : (0 \dots 0) ⟶ V$
4	1	0wlkonlem1	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to (N \in V \land N \in V)$
5	1	1vgrex	$⊢ N \in V \to G \in V$
6	5	adantr	$⊢ (N \in V \land N \in V) \to G \in V$
7	1	0trl	$⊢ G \in V \to (\emptyset Trails (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$
8	4 6 7	3syl	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to (\emptyset Trails (G) P \leftrightarrow P : (0 \dots 0) ⟶ V)$
9	3 8	mpbird	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to \emptyset Trails (G) P$
10		0ex	$⊢ \emptyset \in V$
11	10	a1i	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to \emptyset \in V$
12	1	0wlkonlem2	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to P \in (V ↑_{𝑝𝑚} (0 \dots 0))$
13	1	istrlson	$⊢ ((N \in V \land N \in V) \land (\emptyset \in V \land P \in (V ↑_{𝑝𝑚} (0 \dots 0)))) \to (\emptyset (N TrailsOn (G) N) P \leftrightarrow (\emptyset (N WalksOn (G) N) P \land \emptyset Trails (G) P))$
14	4 11 12 13	syl12anc	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to (\emptyset (N TrailsOn (G) N) P \leftrightarrow (\emptyset (N WalksOn (G) N) P \land \emptyset Trails (G) P))$
15	2 9 14	mpbir2and	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to \emptyset (N TrailsOn (G) N) P$