Metamath Proof Explorer

Theorem 2trld

Description: Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 24-Jan-2021) (Revised by AV, 24-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Hypotheses	2wlkd.p	$⊢ P = ⟨“ A B C ”⟩$
		2wlkd.f	$⊢ F = ⟨“ J K ”⟩$
		2wlkd.s	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
		2wlkd.n	$⊢ φ \to (A \neq B \land B \neq C)$
		2wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
		2wlkd.v	$⊢ V = Vtx (G)$
		2wlkd.i	$⊢ I = iEdg (G)$
		2trld.n	$⊢ φ \to J \neq K$
	Assertion	2trld	$⊢ φ \to F Trails (G) P$

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	$⊢ P = ⟨“ A B C ”⟩$
2		2wlkd.f	$⊢ F = ⟨“ J K ”⟩$
3		2wlkd.s	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
4		2wlkd.n	$⊢ φ \to (A \neq B \land B \neq C)$
5		2wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
6		2wlkd.v	$⊢ V = Vtx (G)$
7		2wlkd.i	$⊢ I = iEdg (G)$
8		2trld.n	$⊢ φ \to J \neq K$
9	1 2 3 4 5 6 7	2wlkd	$⊢ φ \to F Walks (G) P$
10	1 2 3 4 5	2wlkdlem7	$⊢ φ \to (J \in V \land K \in V)$
11		df-3an	$⊢ (J \in V \land K \in V \land J \neq K) \leftrightarrow ((J \in V \land K \in V) \land J \neq K)$
12	10 8 11	sylanbrc	$⊢ φ \to (J \in V \land K \in V \land J \neq K)$
13		funcnvs2	$⊢ (J \in V \land K \in V \land J \neq K) \to Fun {⟨“ J K ”⟩}^{-1}$
14	12 13	syl	$⊢ φ \to Fun {⟨“ J K ”⟩}^{-1}$
15	2	cnveqi	$⊢ F^{-1} = {⟨“ J K ”⟩}^{-1}$
16	15	funeqi	$⊢ Fun F^{-1} \leftrightarrow Fun {⟨“ J K ”⟩}^{-1}$
17	14 16	sylibr	$⊢ φ \to Fun F^{-1}$
18		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
19	9 17 18	sylanbrc	$⊢ φ \to F Trails (G) P$