2pthond

Description: A simple path of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 24-Jan-2021) (Proof shortened by AV, 30-Jan-2021) (Revised by AV, 24-Mar-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$
	2spthd.n	$⊢ φ \to A \neq C$
Assertion	2pthond	$⊢ φ \to F (A SPathsOn (G) C) 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		2spthd.n	$⊢ φ \to A \neq C$
10	1 2 3 4 5 6 7 8	2trlond	$⊢ φ \to F (A TrailsOn (G) C) P$
11	1 2 3 4 5 6 7 8 9	2spthd	$⊢ φ \to F SPaths (G) P$
12		3simpb	$⊢ (A \in V \land B \in V \land C \in V) \to (A \in V \land C \in V)$
13	3 12	syl	$⊢ φ \to (A \in V \land C \in V)$
14		s2cli	$⊢ ⟨“ J K ”⟩ \in Word V$
15	2 14	eqeltri	$⊢ F \in Word V$
16		s3cli	$⊢ ⟨“ A B C ”⟩ \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	6	isspthson	$⊢ ((A \in V \land C \in V) \land (F \in Word V \land P \in Word V)) \to (F (A SPathsOn (G) C) P \leftrightarrow (F (A TrailsOn (G) C) P \land F SPaths (G) P))$
20	13 18 19	sylancl	$⊢ φ \to (F (A SPathsOn (G) C) P \leftrightarrow (F (A TrailsOn (G) C) P \land F SPaths (G) P))$
21	10 11 20	mpbir2and	$⊢ φ \to F (A SPathsOn (G) C) P$

Metamath Proof Explorer

Theorem 2pthond

Proof