3spthd

Description: A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-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)$
	3spthd.n	$⊢ φ \to A \neq D$
Assertion	3spthd	$⊢ φ \to F SPaths (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		3spthd.n	$⊢ φ \to A \neq D$
10	1 2 3 4 5 6 7 8	3trld	$⊢ φ \to F Trails (G) P$
11		simpr	$⊢ (φ \land F Trails (G) P) \to F Trails (G) P$
12		df-3an	$⊢ (A \neq B \land A \neq C \land A \neq D) \leftrightarrow ((A \neq B \land A \neq C) \land A \neq D)$
13	12	simplbi2	$⊢ (A \neq B \land A \neq C) \to (A \neq D \to (A \neq B \land A \neq C \land A \neq D))$
14	13	3ad2ant1	$⊢ ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D) \to (A \neq D \to (A \neq B \land A \neq C \land A \neq D))$
15	9 14	mpan9	$⊢ (φ \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (A \neq B \land A \neq C \land A \neq D)$
16		simpr2	$⊢ (φ \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (B \neq C \land B \neq D)$
17		simpr3	$⊢ (φ \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to C \neq D$
18	15 16 17	3jca	$⊢ (φ \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D) \land C \neq D)$
19	4 18	mpdan	$⊢ φ \to ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D) \land C \neq D)$
20		funcnvs4	$⊢ (((A \in V \land B \in V) \land (C \in V \land D \in V)) \land ((A \neq B \land A \neq C \land A \neq D) \land (B \neq C \land B \neq D) \land C \neq D)) \to Fun {⟨“ A B C D ”⟩}^{-1}$
21	3 19 20	syl2anc	$⊢ φ \to Fun {⟨“ A B C D ”⟩}^{-1}$
22	21	adantr	$⊢ (φ \land F Trails (G) P) \to Fun {⟨“ A B C D ”⟩}^{-1}$
23	1	a1i	$⊢ (φ \land F Trails (G) P) \to P = ⟨“ A B C D ”⟩$
24	23	cnveqd	$⊢ (φ \land F Trails (G) P) \to P^{-1} = {⟨“ A B C D ”⟩}^{-1}$
25	24	funeqd	$⊢ (φ \land F Trails (G) P) \to (Fun P^{-1} \leftrightarrow Fun {⟨“ A B C D ”⟩}^{-1})$
26	22 25	mpbird	$⊢ (φ \land F Trails (G) P) \to Fun P^{-1}$
27		isspth	$⊢ F SPaths (G) P \leftrightarrow (F Trails (G) P \land Fun P^{-1})$
28	11 26 27	sylanbrc	$⊢ (φ \land F Trails (G) P) \to F SPaths (G) P$
29	10 28	mpdan	$⊢ φ \to F SPaths (G) P$

Metamath Proof Explorer

Theorem 3spthd

Proof