3pthond

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

Metamath Proof Explorer

Theorem 3pthond

Proof