umgrwwlks2on

Description: A walk of length 2 between two vertices as word in a multigraph. This theorem would also hold for pseudographs, but to prove this the cases A = B and/or B = C must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021)

	Ref	Expression
Hypotheses	s3wwlks2on.v	$⊢ V = Vtx (G)$
	usgrwwlks2on.e	$⊢ E = Edg (G)$
Assertion	umgrwwlks2on	$⊢ (G \in UMGraph \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\} \in E \land \{B, C\} \in E))$

Proof

Step	Hyp	Ref	Expression
1		s3wwlks2on.v	$⊢ V = Vtx (G)$
2		usgrwwlks2on.e	$⊢ E = Edg (G)$
3		umgrupgr	$⊢ G \in UMGraph \to G \in UPGraph$
4	3	adantr	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to G \in UPGraph$
5		simp1	$⊢ (A \in V \land B \in V \land C \in V) \to A \in V$
6	5	adantl	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to A \in V$
7		simpr3	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to C \in V$
8	1	s3wwlks2on	$⊢ (G \in UPGraph \land A \in V \land C \in V) \to (⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C) \leftrightarrow \exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2))$
9	4 6 7 8	syl3anc	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to (⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C) \leftrightarrow \exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2))$
10		eqid	$⊢ iEdg (G) = iEdg (G)$
11	1 10	upgr2wlk	$⊢ G \in UPGraph \to ((f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2) \leftrightarrow (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} \land iEdg (G) (f (1)) = \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\})))$
12	3 11	syl	$⊢ G \in UMGraph \to ((f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2) \leftrightarrow (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} \land iEdg (G) (f (1)) = \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\})))$
13	12	adantr	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to ((f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2) \leftrightarrow (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} \land iEdg (G) (f (1)) = \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\})))$
14		s3fv0	$⊢ A \in V \to ⟨“ A B C ”⟩ (0) = A$
15	14	3ad2ant1	$⊢ (A \in V \land B \in V \land C \in V) \to ⟨“ A B C ”⟩ (0) = A$
16		s3fv1	$⊢ B \in V \to ⟨“ A B C ”⟩ (1) = B$
17	16	3ad2ant2	$⊢ (A \in V \land B \in V \land C \in V) \to ⟨“ A B C ”⟩ (1) = B$
18	15 17	preq12d	$⊢ (A \in V \land B \in V \land C \in V) \to \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} = \{A, B\}$
19	18	eqeq2d	$⊢ (A \in V \land B \in V \land C \in V) \to (iEdg (G) (f (0)) = \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} \leftrightarrow iEdg (G) (f (0)) = \{A, B\})$
20		s3fv2	$⊢ C \in V \to ⟨“ A B C ”⟩ (2) = C$
21	20	3ad2ant3	$⊢ (A \in V \land B \in V \land C \in V) \to ⟨“ A B C ”⟩ (2) = C$
22	17 21	preq12d	$⊢ (A \in V \land B \in V \land C \in V) \to \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\} = \{B, C\}$
23	22	eqeq2d	$⊢ (A \in V \land B \in V \land C \in V) \to (iEdg (G) (f (1)) = \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\} \leftrightarrow iEdg (G) (f (1)) = \{B, C\})$
24	19 23	anbi12d	$⊢ (A \in V \land B \in V \land C \in V) \to ((iEdg (G) (f (0)) = \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} \land iEdg (G) (f (1)) = \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\}) \leftrightarrow (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))$
25	24	adantl	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to ((iEdg (G) (f (0)) = \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} \land iEdg (G) (f (1)) = \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\}) \leftrightarrow (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))$
26	25	3anbi3d	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to ((f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} \land iEdg (G) (f (1)) = \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\})) \leftrightarrow (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})))$
27		umgruhgr	$⊢ G \in UMGraph \to G \in UHGraph$
28	10	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
29		fdmrn	$⊢ Fun iEdg (G) \leftrightarrow iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G)$
30		simpr	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G)) \to iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G)$
31		id	$⊢ f : (0 ..^2) ⟶ dom iEdg (G) \to f : (0 ..^2) ⟶ dom iEdg (G)$
32		c0ex	$⊢ 0 \in V$
33	32	prid1	$⊢ 0 \in \{0, 1\}$
34		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
35	33 34	eleqtrri	$⊢ 0 \in (0 ..^2)$
36	35	a1i	$⊢ f : (0 ..^2) ⟶ dom iEdg (G) \to 0 \in (0 ..^2)$
37	31 36	ffvelrnd	$⊢ f : (0 ..^2) ⟶ dom iEdg (G) \to f (0) \in dom iEdg (G)$
38	37	adantr	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G)) \to f (0) \in dom iEdg (G)$
39	30 38	ffvelrnd	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G)) \to iEdg (G) (f (0)) \in ran iEdg (G)$
40		1ex	$⊢ 1 \in V$
41	40	prid2	$⊢ 1 \in \{0, 1\}$
42	41 34	eleqtrri	$⊢ 1 \in (0 ..^2)$
43	42	a1i	$⊢ f : (0 ..^2) ⟶ dom iEdg (G) \to 1 \in (0 ..^2)$
44	31 43	ffvelrnd	$⊢ f : (0 ..^2) ⟶ dom iEdg (G) \to f (1) \in dom iEdg (G)$
45	44	adantr	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G)) \to f (1) \in dom iEdg (G)$
46	30 45	ffvelrnd	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G)) \to iEdg (G) (f (1)) \in ran iEdg (G)$
47	39 46	jca	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G)) \to (iEdg (G) (f (0)) \in ran iEdg (G) \land iEdg (G) (f (1)) \in ran iEdg (G))$
48	47	ex	$⊢ f : (0 ..^2) ⟶ dom iEdg (G) \to (iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G) \to (iEdg (G) (f (0)) \in ran iEdg (G) \land iEdg (G) (f (1)) \in ran iEdg (G)))$
49	48	3ad2ant1	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})) \to (iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G) \to (iEdg (G) (f (0)) \in ran iEdg (G) \land iEdg (G) (f (1)) \in ran iEdg (G)))$
50	49	com12	$⊢ iEdg (G) : dom iEdg (G) ⟶ ran iEdg (G) \to ((f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})) \to (iEdg (G) (f (0)) \in ran iEdg (G) \land iEdg (G) (f (1)) \in ran iEdg (G)))$
51	29 50	sylbi	$⊢ Fun iEdg (G) \to ((f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})) \to (iEdg (G) (f (0)) \in ran iEdg (G) \land iEdg (G) (f (1)) \in ran iEdg (G)))$
52	27 28 51	3syl	$⊢ G \in UMGraph \to ((f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})) \to (iEdg (G) (f (0)) \in ran iEdg (G) \land iEdg (G) (f (1)) \in ran iEdg (G)))$
53	52	imp	$⊢ (G \in UMGraph \land (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))) \to (iEdg (G) (f (0)) \in ran iEdg (G) \land iEdg (G) (f (1)) \in ran iEdg (G))$
54		eqcom	$⊢ iEdg (G) (f (0)) = \{A, B\} \leftrightarrow \{A, B\} = iEdg (G) (f (0))$
55	54	biimpi	$⊢ iEdg (G) (f (0)) = \{A, B\} \to \{A, B\} = iEdg (G) (f (0))$
56	55	adantr	$⊢ (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}) \to \{A, B\} = iEdg (G) (f (0))$
57	56	3ad2ant3	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})) \to \{A, B\} = iEdg (G) (f (0))$
58	57	adantl	$⊢ (G \in UMGraph \land (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))) \to \{A, B\} = iEdg (G) (f (0))$
59		edgval	$⊢ Edg (G) = ran iEdg (G)$
60	2 59	eqtri	$⊢ E = ran iEdg (G)$
61	60	a1i	$⊢ (G \in UMGraph \land (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))) \to E = ran iEdg (G)$
62	58 61	eleq12d	$⊢ (G \in UMGraph \land (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))) \to (\{A, B\} \in E \leftrightarrow iEdg (G) (f (0)) \in ran iEdg (G))$
63		eqcom	$⊢ iEdg (G) (f (1)) = \{B, C\} \leftrightarrow \{B, C\} = iEdg (G) (f (1))$
64	63	biimpi	$⊢ iEdg (G) (f (1)) = \{B, C\} \to \{B, C\} = iEdg (G) (f (1))$
65	64	adantl	$⊢ (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}) \to \{B, C\} = iEdg (G) (f (1))$
66	65	3ad2ant3	$⊢ (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})) \to \{B, C\} = iEdg (G) (f (1))$
67	66	adantl	$⊢ (G \in UMGraph \land (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))) \to \{B, C\} = iEdg (G) (f (1))$
68	67 61	eleq12d	$⊢ (G \in UMGraph \land (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))) \to (\{B, C\} \in E \leftrightarrow iEdg (G) (f (1)) \in ran iEdg (G))$
69	62 68	anbi12d	$⊢ (G \in UMGraph \land (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))) \to ((\{A, B\} \in E \land \{B, C\} \in E) \leftrightarrow (iEdg (G) (f (0)) \in ran iEdg (G) \land iEdg (G) (f (1)) \in ran iEdg (G)))$
70	53 69	mpbird	$⊢ (G \in UMGraph \land (f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\}))) \to (\{A, B\} \in E \land \{B, C\} \in E)$
71	70	ex	$⊢ G \in UMGraph \to ((f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})) \to (\{A, B\} \in E \land \{B, C\} \in E))$
72	71	adantr	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to ((f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{A, B\} \land iEdg (G) (f (1)) = \{B, C\})) \to (\{A, B\} \in E \land \{B, C\} \in E))$
73	26 72	sylbid	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to ((f : (0 ..^2) ⟶ dom iEdg (G) \land ⟨“ A B C ”⟩ : (0 \dots 2) ⟶ V \land (iEdg (G) (f (0)) = \{⟨“ A B C ”⟩ (0), ⟨“ A B C ”⟩ (1)\} \land iEdg (G) (f (1)) = \{⟨“ A B C ”⟩ (1), ⟨“ A B C ”⟩ (2)\})) \to (\{A, B\} \in E \land \{B, C\} \in E))$
74	13 73	sylbid	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to ((f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2) \to (\{A, B\} \in E \land \{B, C\} \in E))$
75	74	exlimdv	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to (\exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2) \to (\{A, B\} \in E \land \{B, C\} \in E))$
76	2	umgr2wlk	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))$
77		wlklenvp1	$⊢ f Walks (G) p \to \|p\| = \|f\| + 1$
78		oveq1	$⊢ \|f\| = 2 \to \|f\| + 1 = 2 + 1$
79		2p1e3	$⊢ 2 + 1 = 3$
80	78 79	syl6eq	$⊢ \|f\| = 2 \to \|f\| + 1 = 3$
81	80	adantr	$⊢ (\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to \|f\| + 1 = 3$
82	77 81	sylan9eq	$⊢ (f Walks (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	adantl	$⊢ (\|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	$⊢ (f Walks (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	$⊢ (f Walks (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	80	eqeq2d	$⊢ \|f\| = 2 \to (\|p\| = \|f\| + 1 \leftrightarrow \|p\| = 3)$
93	92	adantl	$⊢ (p \in Word V \land \|f\| = 2) \to (\|p\| = \|f\| + 1 \leftrightarrow \|p\| = 3)$
94		simp1	$⊢ (p \in Word V \land \|p\| = 3 \land (A = p (0) \land B = p (1) \land C = p (2))) \to p \in Word V$
95		oveq2	$⊢ \|p\| = 3 \to (0 ..^\|p\|) = (0 ..^3)$
96		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
97	95 96	syl6eq	$⊢ \|p\| = 3 \to (0 ..^\|p\|) = \{0, 1, 2\}$
98	32	tpid1	$⊢ 0 \in \{0, 1, 2\}$
99		eleq2	$⊢ (0 ..^\|p\|) = \{0, 1, 2\} \to (0 \in (0 ..^\|p\|) \leftrightarrow 0 \in \{0, 1, 2\})$
100	98 99	mpbiri	$⊢ (0 ..^\|p\|) = \{0, 1, 2\} \to 0 \in (0 ..^\|p\|)$
101		wrdsymbcl	$⊢ (p \in Word V \land 0 \in (0 ..^\|p\|)) \to p (0) \in V$
102	100 101	sylan2	$⊢ (p \in Word V \land (0 ..^\|p\|) = \{0, 1, 2\}) \to p (0) \in V$
103	40	tpid2	$⊢ 1 \in \{0, 1, 2\}$
104		eleq2	$⊢ (0 ..^\|p\|) = \{0, 1, 2\} \to (1 \in (0 ..^\|p\|) \leftrightarrow 1 \in \{0, 1, 2\})$
105	103 104	mpbiri	$⊢ (0 ..^\|p\|) = \{0, 1, 2\} \to 1 \in (0 ..^\|p\|)$
106		wrdsymbcl	$⊢ (p \in Word V \land 1 \in (0 ..^\|p\|)) \to p (1) \in V$
107	105 106	sylan2	$⊢ (p \in Word V \land (0 ..^\|p\|) = \{0, 1, 2\}) \to p (1) \in V$
108		2ex	$⊢ 2 \in V$
109	108	tpid3	$⊢ 2 \in \{0, 1, 2\}$
110		eleq2	$⊢ (0 ..^\|p\|) = \{0, 1, 2\} \to (2 \in (0 ..^\|p\|) \leftrightarrow 2 \in \{0, 1, 2\})$
111	109 110	mpbiri	$⊢ (0 ..^\|p\|) = \{0, 1, 2\} \to 2 \in (0 ..^\|p\|)$
112		wrdsymbcl	$⊢ (p \in Word V \land 2 \in (0 ..^\|p\|)) \to p (2) \in V$
113	111 112	sylan2	$⊢ (p \in Word V \land (0 ..^\|p\|) = \{0, 1, 2\}) \to p (2) \in V$
114	102 107 113	3jca	$⊢ (p \in Word V \land (0 ..^\|p\|) = \{0, 1, 2\}) \to (p (0) \in V \land p (1) \in V \land p (2) \in V)$
115	97 114	sylan2	$⊢ (p \in Word V \land \|p\| = 3) \to (p (0) \in V \land p (1) \in V \land p (2) \in V)$
116	115	3adant3	$⊢ (p \in Word V \land \|p\| = 3 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (p (0) \in V \land p (1) \in V \land p (2) \in V)$
117		eleq1	$⊢ A = p (0) \to (A \in V \leftrightarrow p (0) \in V)$
118	117	3ad2ant1	$⊢ (A = p (0) \land B = p (1) \land C = p (2)) \to (A \in V \leftrightarrow p (0) \in V)$
119		eleq1	$⊢ B = p (1) \to (B \in V \leftrightarrow p (1) \in V)$
120	119	3ad2ant2	$⊢ (A = p (0) \land B = p (1) \land C = p (2)) \to (B \in V \leftrightarrow p (1) \in V)$
121		eleq1	$⊢ C = p (2) \to (C \in V \leftrightarrow p (2) \in V)$
122	121	3ad2ant3	$⊢ (A = p (0) \land B = p (1) \land C = p (2)) \to (C \in V \leftrightarrow p (2) \in V)$
123	118 120 122	3anbi123d	$⊢ (A = p (0) \land B = p (1) \land C = p (2)) \to ((A \in V \land B \in V \land C \in V) \leftrightarrow (p (0) \in V \land p (1) \in V \land p (2) \in V))$
124	123	3ad2ant3	$⊢ (p \in Word V \land \|p\| = 3 \land (A = p (0) \land B = p (1) \land C = p (2))) \to ((A \in V \land B \in V \land C \in V) \leftrightarrow (p (0) \in V \land p (1) \in V \land p (2) \in V))$
125	116 124	mpbird	$⊢ (p \in Word V \land \|p\| = 3 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (A \in V \land B \in V \land C \in V)$
126	94 125	jca	$⊢ (p \in Word V \land \|p\| = 3 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (p \in Word V \land (A \in V \land B \in V \land C \in V))$
127	126	3exp	$⊢ p \in Word V \to (\|p\| = 3 \to ((A = p (0) \land B = p (1) \land C = p (2)) \to (p \in Word V \land (A \in V \land B \in V \land C \in V))))$
128	127	adantr	$⊢ (p \in Word V \land \|f\| = 2) \to (\|p\| = 3 \to ((A = p (0) \land B = p (1) \land C = p (2)) \to (p \in Word V \land (A \in V \land B \in V \land C \in V))))$
129	93 128	sylbid	$⊢ (p \in Word V \land \|f\| = 2) \to (\|p\| = \|f\| + 1 \to ((A = p (0) \land B = p (1) \land C = p (2)) \to (p \in Word V \land (A \in V \land B \in V \land C \in V))))$
130	129	impancom	$⊢ (p \in Word V \land \|p\| = \|f\| + 1) \to (\|f\| = 2 \to ((A = p (0) \land B = p (1) \land C = p (2)) \to (p \in Word V \land (A \in V \land B \in V \land C \in V))))$
131	130	impd	$⊢ (p \in Word V \land \|p\| = \|f\| + 1) \to ((\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (p \in Word V \land (A \in V \land B \in V \land C \in V)))$
132	91 77 131	syl2anc	$⊢ f Walks (G) p \to ((\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (p \in Word V \land (A \in V \land B \in V \land C \in V)))$
133	132	imp	$⊢ (f Walks (G) p \land (\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to (p \in Word V \land (A \in V \land B \in V \land C \in V))$
134		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)))$
135	133 134	syl	$⊢ (f Walks (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)))$
136	90 135	mpbird	$⊢ (f Walks (G) p \land (\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to p = ⟨“ A B C ”⟩$
137	136	breq2d	$⊢ (f Walks (G) p \land (\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to (f Walks (G) p \leftrightarrow f Walks (G) ⟨“ A B C ”⟩)$
138	137	biimpd	$⊢ (f Walks (G) p \land (\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to (f Walks (G) p \to f Walks (G) ⟨“ A B C ”⟩)$
139	138	ex	$⊢ f Walks (G) p \to ((\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (f Walks (G) p \to f Walks (G) ⟨“ A B C ”⟩))$
140	139	pm2.43a	$⊢ f Walks (G) p \to ((\|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to f Walks (G) ⟨“ A B C ”⟩)$
141	140	3impib	$⊢ (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to f Walks (G) ⟨“ A B C ”⟩$
142	141	adantl	$⊢ ((A \in V \land B \in V \land C \in V) \land (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to f Walks (G) ⟨“ A B C ”⟩$
143		simpr2	$⊢ ((A \in V \land B \in V \land C \in V) \land (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to \|f\| = 2$
144	142 143	jca	$⊢ ((A \in V \land B \in V \land C \in V) \land (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2)$
145	144	ex	$⊢ (A \in V \land B \in V \land C \in V) \to ((f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2))$
146	145	exlimdv	$⊢ (A \in V \land B \in V \land C \in V) \to (\exists p (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2))$
147	146	eximdv	$⊢ (A \in V \land B \in V \land C \in V) \to (\exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to \exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2))$
148	76 147	syl5com	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to ((A \in V \land B \in V \land C \in V) \to \exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2))$
149	148	3expib	$⊢ G \in UMGraph \to ((\{A, B\} \in E \land \{B, C\} \in E) \to ((A \in V \land B \in V \land C \in V) \to \exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2)))$
150	149	com23	$⊢ G \in UMGraph \to ((A \in V \land B \in V \land C \in V) \to ((\{A, B\} \in E \land \{B, C\} \in E) \to \exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2)))$
151	150	imp	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to ((\{A, B\} \in E \land \{B, C\} \in E) \to \exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2))$
152	75 151	impbid	$⊢ (G \in UMGraph \land (A \in V \land B \in V \land C \in V)) \to (\exists f (f Walks (G) ⟨“ A B C ”⟩ \land \|f\| = 2) \leftrightarrow (\{A, B\} \in E \land \{B, C\} \in E))$
153	9 152	bitrd	$⊢ (G \in UMGraph \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\} \in E \land \{B, C\} \in E))$

Metamath Proof Explorer

Theorem umgrwwlks2on

Proof