Metamath Proof Explorer

Theorem 3trld

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

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

Proof

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