elwspths2spth

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

		Ref	Expression
	Hypothesis	elwwlks2.v	$⊢ V = Vtx (G)$
	Assertion	elwspths2spth	$⊢ G \in UPGraph \to (W \in (2 WSPathsN G) \leftrightarrow \exists a \in V \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$

Proof

Step	Hyp	Ref	Expression
1		elwwlks2.v	$⊢ V = Vtx (G)$
2	1	wspthsnwspthsnon	$⊢ W \in (2 WSPathsN G) \leftrightarrow \exists a \in V \exists c \in V W \in (a (2 WSPathsNOn G) c)$
3	2	a1i	$⊢ G \in UPGraph \to (W \in (2 WSPathsN G) \leftrightarrow \exists a \in V \exists c \in V W \in (a (2 WSPathsNOn G) c))$
4	1	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)))$
5	4	3expb	$⊢ (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)))$
6	5	2rexbidva	$⊢ G \in UPGraph \to (\exists a \in V \exists c \in V W \in (a (2 WSPathsNOn G) c) \leftrightarrow \exists a \in V \exists c \in V \exists b \in V (W = ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c)))$
7		rexcom	$⊢ \exists c \in V \exists b \in V (W = ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c)) \leftrightarrow \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c))$
8		wspthnon	$⊢ ⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c) \leftrightarrow (⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c) \land \exists f f (a SPathsOn (G) c) ⟨“ a b c ”⟩)$
9		ancom	$⊢ (⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c) \land \exists f f (a SPathsOn (G) c) ⟨“ a b c ”⟩) \leftrightarrow (\exists f f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c))$
10		19.41v	$⊢ \exists f (f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c)) \leftrightarrow (\exists f f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c))$
11	9 10	bitr4i	$⊢ (⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c) \land \exists f f (a SPathsOn (G) c) ⟨“ a b c ”⟩) \leftrightarrow \exists f (f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c))$
12		simpr	$⊢ (G \in UPGraph \land a \in V) \to a \in V$
13		simpr	$⊢ (b \in V \land c \in V) \to c \in V$
14	12 13	anim12i	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (a \in V \land c \in V)$
15		vex	$⊢ f \in V$
16		s3cli	$⊢ ⟨“ a b c ”⟩ \in Word V$
17	15 16	pm3.2i	$⊢ (f \in V \land ⟨“ a b c ”⟩ \in Word V)$
18	1	isspthonpth	$⊢ ((a \in V \land c \in V) \land (f \in V \land ⟨“ a b c ”⟩ \in Word V)) \to (f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \leftrightarrow (f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c))$
19	14 17 18	sylancl	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \leftrightarrow (f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c))$
20		wwlknon	$⊢ ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c) \leftrightarrow (⟨“ a b c ”⟩ \in (2 WWalksN G) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)$
21		2nn0	$⊢ 2 \in ℕ_{0}$
22		iswwlksn	$⊢ 2 \in ℕ_{0} \to (⟨“ a b c ”⟩ \in (2 WWalksN G) \leftrightarrow (⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1))$
23	21 22	mp1i	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (⟨“ a b c ”⟩ \in (2 WWalksN G) \leftrightarrow (⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1))$
24	23	3anbi1d	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to ((⟨“ a b c ”⟩ \in (2 WWalksN G) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c) \leftrightarrow ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))$
25	20 24	bitrid	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c) \leftrightarrow ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))$
26	19 25	anbi12d	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to ((f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c)) \leftrightarrow ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)))$
27	26	adantr	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to ((f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c)) \leftrightarrow ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)))$
28	16	a1i	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to ⟨“ a b c ”⟩ \in Word V$
29		simprl1	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land p = ⟨“ a b c ”⟩) \land ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))) \to f SPaths (G) ⟨“ a b c ”⟩$
30		spthiswlk	$⊢ f SPaths (G) ⟨“ a b c ”⟩ \to f Walks (G) ⟨“ a b c ”⟩$
31		wlklenvm1	$⊢ f Walks (G) ⟨“ a b c ”⟩ \to \|f\| = \|⟨“ a b c ”⟩\| - 1$
32		simpl	$⊢ (\|f\| = \|⟨“ a b c ”⟩\| - 1 \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)) \to \|f\| = \|⟨“ a b c ”⟩\| - 1$
33		oveq1	$⊢ \|⟨“ a b c ”⟩\| = 2 + 1 \to \|⟨“ a b c ”⟩\| - 1 = 2 + 1 - 1$
34		2cn	$⊢ 2 \in ℂ$
35		pncan1	$⊢ 2 \in ℂ \to 2 + 1 - 1 = 2$
36	34 35	ax-mp	$⊢ 2 + 1 - 1 = 2$
37	33 36	eqtrdi	$⊢ \|⟨“ a b c ”⟩\| = 2 + 1 \to \|⟨“ a b c ”⟩\| - 1 = 2$
38	37	adantl	$⊢ (⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \to \|⟨“ a b c ”⟩\| - 1 = 2$
39	38	3ad2ant1	$⊢ ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c) \to \|⟨“ a b c ”⟩\| - 1 = 2$
40	39	adantl	$⊢ (\|f\| = \|⟨“ a b c ”⟩\| - 1 \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)) \to \|⟨“ a b c ”⟩\| - 1 = 2$
41	32 40	eqtrd	$⊢ (\|f\| = \|⟨“ a b c ”⟩\| - 1 \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)) \to \|f\| = 2$
42	41	ex	$⊢ \|f\| = \|⟨“ a b c ”⟩\| - 1 \to (((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c) \to \|f\| = 2)$
43	30 31 42	3syl	$⊢ f SPaths (G) ⟨“ a b c ”⟩ \to (((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c) \to \|f\| = 2)$
44	43	3ad2ant1	$⊢ (f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \to (((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c) \to \|f\| = 2)$
45	44	imp	$⊢ ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)) \to \|f\| = 2$
46	45	adantl	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land p = ⟨“ a b c ”⟩) \land ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))) \to \|f\| = 2$
47		s3fv0	$⊢ a \in V \to ⟨“ a b c ”⟩ (0) = a$
48	47	elv	$⊢ ⟨“ a b c ”⟩ (0) = a$
49	48	eqcomi	$⊢ a = ⟨“ a b c ”⟩ (0)$
50		s3fv1	$⊢ b \in V \to ⟨“ a b c ”⟩ (1) = b$
51	50	elv	$⊢ ⟨“ a b c ”⟩ (1) = b$
52	51	eqcomi	$⊢ b = ⟨“ a b c ”⟩ (1)$
53		s3fv2	$⊢ c \in V \to ⟨“ a b c ”⟩ (2) = c$
54	53	elv	$⊢ ⟨“ a b c ”⟩ (2) = c$
55	54	eqcomi	$⊢ c = ⟨“ a b c ”⟩ (2)$
56	49 52 55	3pm3.2i	$⊢ (a = ⟨“ a b c ”⟩ (0) \land b = ⟨“ a b c ”⟩ (1) \land c = ⟨“ a b c ”⟩ (2))$
57	56	a1i	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land p = ⟨“ a b c ”⟩) \land ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))) \to (a = ⟨“ a b c ”⟩ (0) \land b = ⟨“ a b c ”⟩ (1) \land c = ⟨“ a b c ”⟩ (2))$
58	29 46 57	3jca	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land p = ⟨“ a b c ”⟩) \land ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))) \to (f SPaths (G) ⟨“ a b c ”⟩ \land \|f\| = 2 \land (a = ⟨“ a b c ”⟩ (0) \land b = ⟨“ a b c ”⟩ (1) \land c = ⟨“ a b c ”⟩ (2)))$
59		breq2	$⊢ p = ⟨“ a b c ”⟩ \to (f SPaths (G) p \leftrightarrow f SPaths (G) ⟨“ a b c ”⟩)$
60		fveq1	$⊢ p = ⟨“ a b c ”⟩ \to p (0) = ⟨“ a b c ”⟩ (0)$
61	60	eqeq2d	$⊢ p = ⟨“ a b c ”⟩ \to (a = p (0) \leftrightarrow a = ⟨“ a b c ”⟩ (0))$
62		fveq1	$⊢ p = ⟨“ a b c ”⟩ \to p (1) = ⟨“ a b c ”⟩ (1)$
63	62	eqeq2d	$⊢ p = ⟨“ a b c ”⟩ \to (b = p (1) \leftrightarrow b = ⟨“ a b c ”⟩ (1))$
64		fveq1	$⊢ p = ⟨“ a b c ”⟩ \to p (2) = ⟨“ a b c ”⟩ (2)$
65	64	eqeq2d	$⊢ p = ⟨“ a b c ”⟩ \to (c = p (2) \leftrightarrow c = ⟨“ a b c ”⟩ (2))$
66	61 63 65	3anbi123d	$⊢ p = ⟨“ a b c ”⟩ \to ((a = p (0) \land b = p (1) \land c = p (2)) \leftrightarrow (a = ⟨“ a b c ”⟩ (0) \land b = ⟨“ a b c ”⟩ (1) \land c = ⟨“ a b c ”⟩ (2)))$
67	59 66	3anbi13d	$⊢ p = ⟨“ a b c ”⟩ \to ((f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \leftrightarrow (f SPaths (G) ⟨“ a b c ”⟩ \land \|f\| = 2 \land (a = ⟨“ a b c ”⟩ (0) \land b = ⟨“ a b c ”⟩ (1) \land c = ⟨“ a b c ”⟩ (2))))$
68	67	ad2antlr	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land p = ⟨“ a b c ”⟩) \land ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))) \to ((f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \leftrightarrow (f SPaths (G) ⟨“ a b c ”⟩ \land \|f\| = 2 \land (a = ⟨“ a b c ”⟩ (0) \land b = ⟨“ a b c ”⟩ (1) \land c = ⟨“ a b c ”⟩ (2))))$
69	58 68	mpbird	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land p = ⟨“ a b c ”⟩) \land ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))) \to (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))$
70	69	ex	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land p = ⟨“ a b c ”⟩) \to (((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)) \to (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
71	28 70	spcimedv	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)) \to \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
72		spthiswlk	$⊢ f SPaths (G) p \to f Walks (G) p$
73		wlklenvp1	$⊢ f Walks (G) p \to \|p\| = \|f\| + 1$
74		oveq1	$⊢ \|f\| = 2 \to \|f\| + 1 = 2 + 1$
75		2p1e3	$⊢ 2 + 1 = 3$
76	74 75	eqtrdi	$⊢ \|f\| = 2 \to \|f\| + 1 = 3$
77	76	eqeq2d	$⊢ \|f\| = 2 \to (\|p\| = \|f\| + 1 \leftrightarrow \|p\| = 3)$
78	77	biimpcd	$⊢ \|p\| = \|f\| + 1 \to (\|f\| = 2 \to \|p\| = 3)$
79	72 73 78	3syl	$⊢ f SPaths (G) p \to (\|f\| = 2 \to \|p\| = 3)$
80	79	imp	$⊢ (f SPaths (G) p \land \|f\| = 2) \to \|p\| = 3$
81	80	3adant3	$⊢ (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to \|p\| = 3$
82	81	adantl	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \to \|p\| = 3$
83		eqcom	$⊢ a = p (0) \leftrightarrow p (0) = a$
84		eqcom	$⊢ b = p (1) \leftrightarrow p (1) = b$
85		eqcom	$⊢ c = p (2) \leftrightarrow p (2) = c$
86	83 84 85	3anbi123i	$⊢ (a = p (0) \land b = p (1) \land c = p (2)) \leftrightarrow (p (0) = a \land p (1) = b \land p (2) = c)$
87	86	biimpi	$⊢ (a = p (0) \land b = p (1) \land c = p (2)) \to (p (0) = a \land p (1) = b \land p (2) = c)$
88	87	3ad2ant3	$⊢ (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to (p (0) = a \land p (1) = b \land p (2) = c)$
89	88	adantl	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \to (p (0) = a \land p (1) = b \land p (2) = c)$
90	82 89	jca	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \to (\|p\| = 3 \land (p (0) = a \land p (1) = b \land p (2) = c))$
91	1	wlkpwrd	$⊢ f Walks (G) p \to p \in Word V$
92	72 91	syl	$⊢ f SPaths (G) p \to p \in Word V$
93	92	3ad2ant1	$⊢ (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to p \in Word V$
94	12	anim1i	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (a \in V \land (b \in V \land c \in V))$
95		3anass	$⊢ (a \in V \land b \in V \land c \in V) \leftrightarrow (a \in V \land (b \in V \land c \in V))$
96	94 95	sylibr	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (a \in V \land b \in V \land c \in V)$
97		eqwrds3	$⊢ (p \in Word V \land (a \in V \land b \in V \land c \in V)) \to (p = ⟨“ a b c ”⟩ \leftrightarrow (\|p\| = 3 \land (p (0) = a \land p (1) = b \land p (2) = c)))$
98	93 96 97	syl2anr	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \to (p = ⟨“ a b c ”⟩ \leftrightarrow (\|p\| = 3 \land (p (0) = a \land p (1) = b \land p (2) = c)))$
99	90 98	mpbird	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \to p = ⟨“ a b c ”⟩$
100	59	biimpcd	$⊢ f SPaths (G) p \to (p = ⟨“ a b c ”⟩ \to f SPaths (G) ⟨“ a b c ”⟩)$
101	100	3ad2ant1	$⊢ (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to (p = ⟨“ a b c ”⟩ \to f SPaths (G) ⟨“ a b c ”⟩)$
102	101	adantl	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \to (p = ⟨“ a b c ”⟩ \to f SPaths (G) ⟨“ a b c ”⟩)$
103	102	imp	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to f SPaths (G) ⟨“ a b c ”⟩$
104	48	a1i	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to ⟨“ a b c ”⟩ (0) = a$
105		fveq2	$⊢ \|f\| = 2 \to ⟨“ a b c ”⟩ (\|f\|) = ⟨“ a b c ”⟩ (2)$
106	105 54	eqtrdi	$⊢ \|f\| = 2 \to ⟨“ a b c ”⟩ (\|f\|) = c$
107	106	3ad2ant2	$⊢ (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to ⟨“ a b c ”⟩ (\|f\|) = c$
108	107	ad2antlr	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to ⟨“ a b c ”⟩ (\|f\|) = c$
109	103 104 108	3jca	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to (f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c)$
110		wlkiswwlks1	$⊢ G \in UPGraph \to (f Walks (G) p \to p \in WWalks (G))$
111	110	adantr	$⊢ (G \in UPGraph \land a \in V) \to (f Walks (G) p \to p \in WWalks (G))$
112	111	adantr	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (f Walks (G) p \to p \in WWalks (G))$
113	72 112	syl5com	$⊢ f SPaths (G) p \to (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to p \in WWalks (G))$
114	113	3ad2ant1	$⊢ (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to p \in WWalks (G))$
115	114	impcom	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \to p \in WWalks (G)$
116	115	adantr	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to p \in WWalks (G)$
117		eleq1	$⊢ p = ⟨“ a b c ”⟩ \to (p \in WWalks (G) \leftrightarrow ⟨“ a b c ”⟩ \in WWalks (G))$
118	117	bicomd	$⊢ p = ⟨“ a b c ”⟩ \to (⟨“ a b c ”⟩ \in WWalks (G) \leftrightarrow p \in WWalks (G))$
119	118	adantl	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to (⟨“ a b c ”⟩ \in WWalks (G) \leftrightarrow p \in WWalks (G))$
120	116 119	mpbird	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to ⟨“ a b c ”⟩ \in WWalks (G)$
121		s3len	$⊢ \|⟨“ a b c ”⟩\| = 3$
122		df-3	$⊢ 3 = 2 + 1$
123	121 122	eqtri	$⊢ \|⟨“ a b c ”⟩\| = 2 + 1$
124	120 123	jctir	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to (⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1)$
125	54	a1i	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to ⟨“ a b c ”⟩ (2) = c$
126	124 104 125	3jca	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)$
127	109 126	jca	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \land p = ⟨“ a b c ”⟩) \to ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))$
128	99 127	mpdan	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))) \to ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c))$
129	128	ex	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to ((f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)))$
130	129	exlimdv	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (\exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to ((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)))$
131	71 130	impbid	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)) \leftrightarrow \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
132	131	adantr	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (((f SPaths (G) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (\|f\|) = c) \land ((⟨“ a b c ”⟩ \in WWalks (G) \land \|⟨“ a b c ”⟩\| = 2 + 1) \land ⟨“ a b c ”⟩ (0) = a \land ⟨“ a b c ”⟩ (2) = c)) \leftrightarrow \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
133	27 132	bitrd	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to ((f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c)) \leftrightarrow \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
134	133	exbidv	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (\exists f (f (a SPathsOn (G) c) ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c)) \leftrightarrow \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
135	11 134	bitrid	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to ((⟨“ a b c ”⟩ \in (a (2 WWalksNOn G) c) \land \exists f f (a SPathsOn (G) c) ⟨“ a b c ”⟩) \leftrightarrow \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
136	8 135	bitrid	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c) \leftrightarrow \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
137	136	pm5.32da	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to ((W = ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c)) \leftrightarrow (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$
138	137	2rexbidva	$⊢ (G \in UPGraph \land a \in V) \to (\exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c)) \leftrightarrow \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$
139	7 138	bitrid	$⊢ (G \in UPGraph \land a \in V) \to (\exists c \in V \exists b \in V (W = ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c)) \leftrightarrow \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$
140	139	rexbidva	$⊢ G \in UPGraph \to (\exists a \in V \exists c \in V \exists b \in V (W = ⟨“ a b c ”⟩ \land ⟨“ a b c ”⟩ \in (a (2 WSPathsNOn G) c)) \leftrightarrow \exists a \in V \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$
141	3 6 140	3bitrd	$⊢ G \in UPGraph \to (W \in (2 WSPathsN G) \leftrightarrow \exists a \in V \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f SPaths (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$

Metamath Proof Explorer

Theorem elwspths2spth

Proof