Metamath Proof Explorer

Theorem 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 ∈ UMGraph ∧ 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 umgrupgr ⊢ G ∈ UMGraph → G ∈ UPGraph
4 3 adantr ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → G ∈ UPGraph
5 simp1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V
6 5 adantl ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V
7 simpr3 ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V
8 1 s3wwlks2on ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
9 4 6 7 8 syl3anc ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
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 3 11 syl ⊢ G ∈ UMGraph → 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 umgruhgr ⊢ G ∈ UMGraph → 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 ∈ UMGraph → 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph → 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ 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 ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2 → A B ∈ E ∧ B C ∈ E
71 70 exlimdv ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2 → A B ∈ E ∧ B C ∈ E
72 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
73 wlklenvp1 ⊢ f Walks ⁡ G p → p = f + 1
74 oveq1 ⊢ f = 2 → f + 1 = 2 + 1
75 2p1e3 ⊢ 2 + 1 = 3
76 74 75 eqtrdi ⊢ f = 2 → f + 1 = 3
77 76 adantr ⊢ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f + 1 = 3
78 73 77 sylan9eq ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p = 3
79 eqcom ⊢ A = p ⁡ 0 ↔ p ⁡ 0 = A
80 eqcom ⊢ B = p ⁡ 1 ↔ p ⁡ 1 = B
81 eqcom ⊢ C = p ⁡ 2 ↔ p ⁡ 2 = C
82 79 80 81 3anbi123i ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 ↔ p ⁡ 0 = A ∧ p ⁡ 1 = B ∧ p ⁡ 2 = C
83 82 bilani ⊢ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ 0 = A ∧ p ⁡ 1 = B ∧ p ⁡ 2 = C
84 83 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
85 78 84 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
86 1 wlkpwrd ⊢ f Walks ⁡ G p → p ∈ Word V
87 76 eqeq2d ⊢ f = 2 → p = f + 1 ↔ p = 3
88 87 adantl ⊢ p ∈ Word V ∧ f = 2 → p = f + 1 ↔ p = 3
89 simp1 ⊢ p ∈ Word V ∧ p = 3 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ∈ Word V
90 oveq2 ⊢ p = 3 → 0 ..^ p = 0 ..^ 3
91 fzo0to3tp ⊢ 0 ..^ 3 = 0 1 2
92 90 91 eqtrdi ⊢ p = 3 → 0 ..^ p = 0 1 2
93 c0ex ⊢ 0 ∈ V
94 93 tpid1 ⊢ 0 ∈ 0 1 2
95 eleq2 ⊢ 0 ..^ p = 0 1 2 → 0 ∈ 0 ..^ p ↔ 0 ∈ 0 1 2
96 94 95 mpbiri ⊢ 0 ..^ p = 0 1 2 → 0 ∈ 0 ..^ p
97 wrdsymbcl ⊢ p ∈ Word V ∧ 0 ∈ 0 ..^ p → p ⁡ 0 ∈ V
98 96 97 sylan2 ⊢ p ∈ Word V ∧ 0 ..^ p = 0 1 2 → p ⁡ 0 ∈ V
99 1eltp012 ⊢ 1 ∈ 0 1 2
100 eleq2 ⊢ 0 ..^ p = 0 1 2 → 1 ∈ 0 ..^ p ↔ 1 ∈ 0 1 2
101 99 100 mpbiri ⊢ 0 ..^ p = 0 1 2 → 1 ∈ 0 ..^ p
102 wrdsymbcl ⊢ p ∈ Word V ∧ 1 ∈ 0 ..^ p → p ⁡ 1 ∈ V
103 101 102 sylan2 ⊢ p ∈ Word V ∧ 0 ..^ p = 0 1 2 → p ⁡ 1 ∈ V
104 2ex ⊢ 2 ∈ V
105 104 tpid3 ⊢ 2 ∈ 0 1 2
106 eleq2 ⊢ 0 ..^ p = 0 1 2 → 2 ∈ 0 ..^ p ↔ 2 ∈ 0 1 2
107 105 106 mpbiri ⊢ 0 ..^ p = 0 1 2 → 2 ∈ 0 ..^ p
108 wrdsymbcl ⊢ p ∈ Word V ∧ 2 ∈ 0 ..^ p → p ⁡ 2 ∈ V
109 107 108 sylan2 ⊢ p ∈ Word V ∧ 0 ..^ p = 0 1 2 → p ⁡ 2 ∈ V
110 98 103 109 3jca ⊢ p ∈ Word V ∧ 0 ..^ p = 0 1 2 → p ⁡ 0 ∈ V ∧ p ⁡ 1 ∈ V ∧ p ⁡ 2 ∈ V
111 92 110 sylan2 ⊢ p ∈ Word V ∧ p = 3 → p ⁡ 0 ∈ V ∧ p ⁡ 1 ∈ V ∧ p ⁡ 2 ∈ V
112 111 3adant3 ⊢ p ∈ Word V ∧ p = 3 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ⁡ 0 ∈ V ∧ p ⁡ 1 ∈ V ∧ p ⁡ 2 ∈ V
113 eleq1 ⊢ A = p ⁡ 0 → A ∈ V ↔ p ⁡ 0 ∈ V
114 113 3ad2ant1 ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → A ∈ V ↔ p ⁡ 0 ∈ V
115 eleq1 ⊢ B = p ⁡ 1 → B ∈ V ↔ p ⁡ 1 ∈ V
116 115 3ad2ant2 ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → B ∈ V ↔ p ⁡ 1 ∈ V
117 eleq1 ⊢ C = p ⁡ 2 → C ∈ V ↔ p ⁡ 2 ∈ V
118 117 3ad2ant3 ⊢ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → C ∈ V ↔ p ⁡ 2 ∈ V
119 114 116 118 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
120 119 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
121 112 120 mpbird ⊢ p ∈ Word V ∧ p = 3 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → A ∈ V ∧ B ∈ V ∧ C ∈ V
122 89 121 jca ⊢ p ∈ Word V ∧ p = 3 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ∈ Word V ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V
123 122 3exp ⊢ p ∈ Word V → p = 3 → A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p ∈ Word V ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V
124 123 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
125 88 124 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
126 125 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
127 126 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
128 86 73 127 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
129 128 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
130 eqwrds3 ⊢ p ∈ Word V ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → p = ⟨“ ABC ”⟩ ↔ p = 3 ∧ p ⁡ 0 = A ∧ p ⁡ 1 = B ∧ p ⁡ 2 = C
131 129 130 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
132 85 131 mpbird ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → p = ⟨“ ABC ”⟩
133 132 breq2d ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p ↔ f Walks ⁡ G ⟨“ ABC ”⟩
134 133 biimpd ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p → f Walks ⁡ G ⟨“ ABC ”⟩
135 134 ex ⊢ f Walks ⁡ G p → f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G p → f Walks ⁡ G ⟨“ ABC ”⟩
136 135 pm2.43a ⊢ f Walks ⁡ G p → f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G ⟨“ ABC ”⟩
137 136 3impib ⊢ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f Walks ⁡ G ⟨“ ABC ”⟩
138 137 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 ”⟩
139 simpr2 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ f Walks ⁡ G p ∧ f = 2 ∧ A = p ⁡ 0 ∧ B = p ⁡ 1 ∧ C = p ⁡ 2 → f = 2
140 138 139 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
141 140 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
142 141 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
143 142 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
144 72 143 syl5com ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
145 144 3expib ⊢ G ∈ UMGraph → A B ∈ E ∧ B C ∈ E → A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
146 145 com23 ⊢ G ∈ UMGraph → A ∈ V ∧ B ∈ V ∧ C ∈ V → A B ∈ E ∧ B C ∈ E → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
147 146 imp ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A B ∈ E ∧ B C ∈ E → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
148 71 147 impbid ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2 ↔ A B ∈ E ∧ B C ∈ E
149 9 148 bitrd ⊢ G ∈ UMGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ A B ∈ E ∧ B C ∈ E