elwspths2on

Description: A simple path of length 2 between two vertices (in a graph) as length 3 string. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 16-Mar-2022)

		Ref	Expression
	Hypothesis	elwwlks2on.v	$⊢ V = Vtx (G)$
	Assertion	elwspths2on	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (W \in (A (2 WSPathsNOn G) C) \leftrightarrow \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))$

Proof

Step	Hyp	Ref	Expression
1		elwwlks2on.v	$⊢ V = Vtx (G)$
2		wspthnon	$⊢ W \in (A (2 WSPathsNOn G) C) \leftrightarrow (W \in (A (2 WWalksNOn G) C) \land \exists f f (A SPathsOn (G) C) W)$
3	2	biimpi	$⊢ W \in (A (2 WSPathsNOn G) C) \to (W \in (A (2 WWalksNOn G) C) \land \exists f f (A SPathsOn (G) C) W)$
4	1	elwwlks2on	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (W \in (A (2 WWalksNOn G) C) \leftrightarrow \exists b \in V (W = ⟨“ A b C ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)))$
5		simpl	$⊢ (W = ⟨“ A b C ”⟩ \land W \in (A (2 WSPathsNOn G) C)) \to W = ⟨“ A b C ”⟩$
6		eleq1	$⊢ W = ⟨“ A b C ”⟩ \to (W \in (A (2 WSPathsNOn G) C) \leftrightarrow ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C))$
7	6	biimpa	$⊢ (W = ⟨“ A b C ”⟩ \land W \in (A (2 WSPathsNOn G) C)) \to ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)$
8	5 7	jca	$⊢ (W = ⟨“ A b C ”⟩ \land W \in (A (2 WSPathsNOn G) C)) \to (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C))$
9	8	ex	$⊢ W = ⟨“ A b C ”⟩ \to (W \in (A (2 WSPathsNOn G) C) \to (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))$
10	9	adantr	$⊢ (W = ⟨“ A b C ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \to (W \in (A (2 WSPathsNOn G) C) \to (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))$
11	10	com12	$⊢ W \in (A (2 WSPathsNOn G) C) \to ((W = ⟨“ A b C ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \to (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))$
12	11	reximdv	$⊢ W \in (A (2 WSPathsNOn G) C) \to (\exists b \in V (W = ⟨“ A b C ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \to \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))$
13	12	a1i13	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (W \in (A (2 WSPathsNOn G) C) \to (\exists f f (A SPathsOn (G) C) W \to (\exists b \in V (W = ⟨“ A b C ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \to \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))))$
14	13	com24	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (\exists b \in V (W = ⟨“ A b C ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \to (\exists f f (A SPathsOn (G) C) W \to (W \in (A (2 WSPathsNOn G) C) \to \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))))$
15	4 14	sylbid	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (W \in (A (2 WWalksNOn G) C) \to (\exists f f (A SPathsOn (G) C) W \to (W \in (A (2 WSPathsNOn G) C) \to \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))))$
16	15	impd	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to ((W \in (A (2 WWalksNOn G) C) \land \exists f f (A SPathsOn (G) C) W) \to (W \in (A (2 WSPathsNOn G) C) \to \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C))))$
17	16	com23	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (W \in (A (2 WSPathsNOn G) C) \to ((W \in (A (2 WWalksNOn G) C) \land \exists f f (A SPathsOn (G) C) W) \to \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C))))$
18	3 17	mpdi	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (W \in (A (2 WSPathsNOn G) C) \to \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))$
19	6	biimpar	$⊢ (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)) \to W \in (A (2 WSPathsNOn G) C)$
20	19	a1i	$⊢ ((G \in UPGraph \land A \in V \land C \in V) \land b \in V) \to ((W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)) \to W \in (A (2 WSPathsNOn G) C))$
21	20	rexlimdva	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (\exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)) \to W \in (A (2 WSPathsNOn G) C))$
22	18 21	impbid	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (W \in (A (2 WSPathsNOn G) C) \leftrightarrow \exists b \in V (W = ⟨“ A b C ”⟩ \land ⟨“ A b C ”⟩ \in (A (2 WSPathsNOn G) C)))$

Metamath Proof Explorer

Theorem elwspths2on

Proof