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 birani ⊢ iEdg ⁡ G ⁡ f ⁡ 0 = A B ∧ iEdg ⁡ G ⁡ f ⁡ 1 = B C → A B = iEdg ⁡ G ⁡ f ⁡ 0
56 55 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
57 56 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
58 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
59 2 58 eqtri ⊢ E = ran ⁡ iEdg ⁡ G
60 59 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
61 57 60 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
62 eqcom ⊢ iEdg ⁡ G ⁡ f ⁡ 1 = B C ↔ B C = iEdg ⁡ G ⁡ f ⁡ 1
63 62 bilani ⊢ iEdg ⁡ G ⁡ f ⁡ 0 = A B ∧ iEdg ⁡ G ⁡ f ⁡ 1 = B C → B C = iEdg ⁡ G ⁡ f ⁡ 1
64 63 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
65 64 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
66 65 60 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
67 61 66 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
68 53 67 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
69 68 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
70 69 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
71 26 70 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
72 13 71 sylbid ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2 → A B ∈ E ∧ B C ∈ E
73 72 exlimdv ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2 → A B ∈ E ∧ B C ∈ E
74 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
75 74 3ad2ant1 ⊢ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E → G ∈ UMGraph
76 simp2 ⊢ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E → A B ∈ E
77 simp3 ⊢ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E → B C ∈ E
78 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
79 75 76 77 78 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
80 wlklenvp1 ⊢ f Walks ⁡ G p → p = f + 1
81 oveq1 ⊢ f = 2 → f + 1 = 2 + 1
82 2p1e3 ⊢ 2 + 1 = 3
83 81 82 eqtrdi ⊢ f = 2 → f + 1 = 3
84 83 adantr ⊢ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f + 1 = 3
85 80 84 sylan9eq ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p = 3
86 eqcom ⊢ A = p ⁡ 0 ↔ p ⁡ 0 = A
87 eqcom ⊢ B = p ⁡ 1 ↔ p ⁡ 1 = B
88 eqcom ⊢ C = p ⁡ 2 ↔ p ⁡ 2 = C
89 86 87 88 3anbi123i ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 ↔ p ⁡ 0 = A ∧ p ⁡ 1 = B ∧ p ⁡ 2 = C
90 89 bilani ⊢ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ 0 = A ∧ p ⁡ 1 = B ∧ p ⁡ 2 = C
91 90 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
92 85 91 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
93 1 wlkpwrd ⊢ f Walks ⁡ G p → p ∈ Word V
94 83 eqeq2d ⊢ f = 2 → p = f + 1 ↔ p = 3
95 94 adantl ⊢ p ∈ Word V ∧ f = 2 → p = f + 1 ↔ p = 3
96 simp1 ⊢ p ∈ Word V ∧ p = 3 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ∈ Word V
97 oveq2 ⊢ p = 3 → 0 ..^ p = 0 ..^ 3
98 fzo0to3tp ⊢ 0 ..^ 3 = 0 1 2
99 97 98 eqtrdi ⊢ p = 3 → 0 ..^ p = 0 1 2
100 32 tpid1 ⊢ 0 ∈ 0 1 2
101 eleq2 ⊢ 0 ..^ p = 0 1 2 → 0 ∈ 0 ..^ p ↔ 0 ∈ 0 1 2
102 100 101 mpbiri ⊢ 0 ..^ p = 0 1 2 → 0 ∈ 0 ..^ p
103 wrdsymbcl ⊢ p ∈ Word V ∧ 0 ∈ 0 ..^ p → p ⁡ 0 ∈ V
104 102 103 sylan2 ⊢ p ∈ Word V ∧ 0 ..^ p = 0 1 2 → p ⁡ 0 ∈ V
105 40 tpid2 ⊢ 1 ∈ 0 1 2
106 eleq2 ⊢ 0 ..^ p = 0 1 2 → 1 ∈ 0 ..^ p ↔ 1 ∈ 0 1 2
107 105 106 mpbiri ⊢ 0 ..^ p = 0 1 2 → 1 ∈ 0 ..^ p
108 wrdsymbcl ⊢ p ∈ Word V ∧ 1 ∈ 0 ..^ p → p ⁡ 1 ∈ V
109 107 108 sylan2 ⊢ p ∈ Word V ∧ 0 ..^ p = 0 1 2 → p ⁡ 1 ∈ V
110 2ex ⊢ 2 ∈ V
111 110 tpid3 ⊢ 2 ∈ 0 1 2
112 eleq2 ⊢ 0 ..^ p = 0 1 2 → 2 ∈ 0 ..^ p ↔ 2 ∈ 0 1 2
113 111 112 mpbiri ⊢ 0 ..^ p = 0 1 2 → 2 ∈ 0 ..^ p
114 wrdsymbcl ⊢ p ∈ Word V ∧ 2 ∈ 0 ..^ p → p ⁡ 2 ∈ V
115 113 114 sylan2 ⊢ p ∈ Word V ∧ 0 ..^ p = 0 1 2 → p ⁡ 2 ∈ V
116 104 109 115 3jca ⊢ p ∈ Word V ∧ 0 ..^ p = 0 1 2 → p ⁡ 0 ∈ V ∧ p ⁡ 1 ∈ V ∧ p ⁡ 2 ∈ V
117 99 116 sylan2 ⊢ p ∈ Word V ∧ p = 3 → p ⁡ 0 ∈ V ∧ p ⁡ 1 ∈ V ∧ p ⁡ 2 ∈ V
118 117 3adant3 ⊢ p ∈ Word V ∧ p = 3 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ 0 ∈ V ∧ p ⁡ 1 ∈ V ∧ p ⁡ 2 ∈ V
119 eleq1 ⊢ A = p ⁡ 0 → A ∈ V ↔ p ⁡ 0 ∈ V
120 119 3ad2ant1 ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → A ∈ V ↔ p ⁡ 0 ∈ V
121 eleq1 ⊢ B = p ⁡ 1 → B ∈ V ↔ p ⁡ 1 ∈ V
122 121 3ad2ant2 ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → B ∈ V ↔ p ⁡ 1 ∈ V
123 eleq1 ⊢ C = p ⁡ 2 → C ∈ V ↔ p ⁡ 2 ∈ V
124 123 3ad2ant3 ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → C ∈ V ↔ p ⁡ 2 ∈ V
125 120 122 124 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
126 125 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
127 118 126 mpbird ⊢ p ∈ Word V ∧ p = 3 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → A ∈ V ∧ B ∈ V ∧ C ∈ V
128 96 127 jca ⊢ p ∈ Word V ∧ p = 3 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ∈ Word V ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V
129 128 3exp ⊢ p ∈ Word V → p = 3 → A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ∈ Word V ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V
130 129 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
131 95 130 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
132 131 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
133 132 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
134 93 80 133 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
135 134 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
136 eqwrds3 ⊢ p ∈ Word V ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → p = ⟨“ ABC ”⟩ ↔ p = 3 ∧ p ⁡ 0 = A ∧ p ⁡ 1 = B ∧ p ⁡ 2 = C
137 135 136 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
138 92 137 mpbird ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p = ⟨“ ABC ”⟩
139 138 breq2d ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p ↔ f Walks ⁡ G ⟨“ ABC ”⟩
140 139 biimpd ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p → f Walks ⁡ G ⟨“ ABC ”⟩
141 140 ex ⊢ f Walks ⁡ G p → f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p → f Walks ⁡ G ⟨“ ABC ”⟩
142 141 pm2.43a ⊢ f Walks ⁡ G p → f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G ⟨“ ABC ”⟩
143 142 3impib ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G ⟨“ ABC ”⟩
144 143 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 ”⟩
145 simpr2 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f = 2
146 144 145 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
147 146 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
148 147 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
149 148 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
150 79 149 syl5com ⊢ G ∈ USGraph ∧ A B ∈ E ∧ B C ∈ E → A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
151 150 3expib ⊢ G ∈ USGraph → A B ∈ E ∧ B C ∈ E → A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
152 151 com23 ⊢ G ∈ USGraph → A ∈ V ∧ B ∈ V ∧ C ∈ V → A B ∈ E ∧ B C ∈ E → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
153 152 imp ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A B ∈ E ∧ B C ∈ E → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
154 73 153 impbid ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2 ↔ A B ∈ E ∧ B C ∈ E
155 8 154 bitrd ⊢ G ∈ USGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ A B ∈ E ∧ B C ∈ E