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