1trld

Description: In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 22-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypotheses	1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
	1wlkd.f	$⊢ F = ⟨“ J ”⟩$
	1wlkd.x	$⊢ φ \to X \in V$
	1wlkd.y	$⊢ φ \to Y \in V$
	1wlkd.l	$⊢ (φ \land X = Y) \to I (J) = \{X\}$
	1wlkd.j	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq I (J)$
	1wlkd.v	$⊢ V = Vtx (G)$
	1wlkd.i	$⊢ I = iEdg (G)$
Assertion	1trld	$⊢ φ \to F Trails (G) P$

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
2		1wlkd.f	$⊢ F = ⟨“ J ”⟩$
3		1wlkd.x	$⊢ φ \to X \in V$
4		1wlkd.y	$⊢ φ \to Y \in V$
5		1wlkd.l	$⊢ (φ \land X = Y) \to I (J) = \{X\}$
6		1wlkd.j	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq I (J)$
7		1wlkd.v	$⊢ V = Vtx (G)$
8		1wlkd.i	$⊢ I = iEdg (G)$
9	1 2 3 4 5 6 7 8	1wlkd	$⊢ φ \to F Walks (G) P$
10		funcnvs1	$⊢ Fun {⟨“ J ”⟩}^{-1}$
11	2	cnveqi	$⊢ F^{-1} = {⟨“ J ”⟩}^{-1}$
12	11	funeqi	$⊢ Fun F^{-1} \leftrightarrow Fun {⟨“ J ”⟩}^{-1}$
13	10 12	mpbir	$⊢ Fun F^{-1}$
14		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
15	9 13 14	sylanblrc	$⊢ φ \to F Trails (G) P$

Metamath Proof Explorer

Theorem 1trld

Proof