Metamath Proof Explorer

Theorem usgrwwlks2on

Description: A walk of length 2 between two vertices as word in a simple graph. This theorem is analogous to umgrwwlks2on except it talks about simple graphs and therefore does not require the Axiom of Choice for its proof. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses s3wwlks2on.v ⊢ V = Vtx ⁡ G
usgrwwlks2on.e ⊢ E = Edg ⁡ G
Assertion usgrwwlks2on ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ A B ∈ E ∧ B C ∈ E

Proof

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