3spthond

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)

	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	3spthond	$⊢ φ \to F (A SPathsOn (G) D) 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	3trlond	$⊢ φ \to F (A TrailsOn (G) D) P$
11	1 2 3 4 5 6 7 8 9	3spthd	$⊢ φ \to F SPaths (G) P$
12	3	simplld	$⊢ φ \to A \in V$
13	3	simprrd	$⊢ φ \to D \in V$
14		s3cli	$⊢ ⟨“ J K L ”⟩ \in Word V$
15	2 14	eqeltri	$⊢ F \in Word V$
16		s4cli	$⊢ ⟨“ A B C D ”⟩ \in Word V$
17	1 16	eqeltri	$⊢ P \in Word V$
18	15 17	pm3.2i	$⊢ (F \in Word V \land P \in Word V)$
19	18	a1i	$⊢ φ \to (F \in Word V \land P \in Word V)$
20	6	isspthson	$⊢ ((A \in V \land D \in V) \land (F \in Word V \land P \in Word V)) \to (F (A SPathsOn (G) D) P \leftrightarrow (F (A TrailsOn (G) D) P \land F SPaths (G) P))$
21	12 13 19 20	syl21anc	$⊢ φ \to (F (A SPathsOn (G) D) P \leftrightarrow (F (A TrailsOn (G) D) P \land F SPaths (G) P))$
22	10 11 21	mpbir2and	$⊢ φ \to F (A SPathsOn (G) D) P$

Metamath Proof Explorer

Theorem 3spthond

Proof