Metamath Proof Explorer

Theorem elwspths2spth

Description: A simple path of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 28-Feb-2018) (Revised by AV, 18-May-2021) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypothesis elwwlks2.v ⊢ V = Vtx ⁡ G
Assertion elwspths2spth ⊢ G ∈ UPGraph → W ∈ 2 WSPathsN G ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ ∧ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2

Proof

Step Hyp Ref Expression
1 elwwlks2.v ⊢ V = Vtx ⁡ G
2 1 wspthsnwspthsnon ⊢ W ∈ 2 WSPathsN G ↔ ∃ a ∈ V ∃ c ∈ V W ∈ a 2 WSPathsNOn G c
3 2 a1i ⊢ G ∈ UPGraph → W ∈ 2 WSPathsN G ↔ ∃ a ∈ V ∃ c ∈ V W ∈ a 2 WSPathsNOn G c
4 1 elwspths2on ⊢ G ∈ UPGraph ∧ a ∈ V ∧ c ∈ V → W ∈ a 2 WSPathsNOn G c ↔ ∃ b ∈ V W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c
5 4 3expb ⊢ G ∈ UPGraph ∧ a ∈ V ∧ c ∈ V → W ∈ a 2 WSPathsNOn G c ↔ ∃ b ∈ V W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c
6 5 2rexbidva ⊢ G ∈ UPGraph → ∃ a ∈ V ∃ c ∈ V W ∈ a 2 WSPathsNOn G c ↔ ∃ a ∈ V ∃ c ∈ V ∃ b ∈ V W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c
7 rexcom ⊢ ∃ c ∈ V ∃ b ∈ V W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c ↔ ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c
8 wspthnon ⊢ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c ↔ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ∧ ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩
9 ancom ⊢ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ∧ ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ↔ ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c
10 19.41v ⊢ ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ↔ ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c
11 9 10 bitr4i ⊢ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ∧ ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ↔ ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c
12 simpr ⊢ G ∈ UPGraph ∧ a ∈ V → a ∈ V
13 simpr ⊢ b ∈ V ∧ c ∈ V → c ∈ V
14 12 13 anim12i ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → a ∈ V ∧ c ∈ V
15 vex ⊢ f ∈ V
16 s3cli ⊢ ⟨“ abc ”⟩ ∈ Word V
17 15 16 pm3.2i ⊢ f ∈ V ∧ ⟨“ abc ”⟩ ∈ Word V
18 1 isspthonpth ⊢ a ∈ V ∧ c ∈ V ∧ f ∈ V ∧ ⟨“ abc ”⟩ ∈ Word V → f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ↔ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c
19 14 17 18 sylancl ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ↔ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c
20 wwlknon ⊢ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ↔ ⟨“ abc ”⟩ ∈ 2 WWalksN G ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
21 2nn0 ⊢ 2 ∈ ℕ 0
22 iswwlksn ⊢ 2 ∈ ℕ 0 → ⟨“ abc ”⟩ ∈ 2 WWalksN G ↔ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1
23 21 22 mp1i ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → ⟨“ abc ”⟩ ∈ 2 WWalksN G ↔ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1
24 23 3anbi1d ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → ⟨“ abc ”⟩ ∈ 2 WWalksN G ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c ↔ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
25 20 24 bitrid ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ↔ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
26 19 25 anbi12d ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ↔ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
27 26 adantr ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ W = ⟨“ abc ”⟩ → f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ↔ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
28 16 a1i ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → ⟨“ abc ”⟩ ∈ Word V
29 simprl1 ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ p = ⟨“ abc ”⟩ ∧ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f SPaths ⁡ G ⟨“ abc ”⟩
30 spthiswlk ⊢ f SPaths ⁡ G ⟨“ abc ”⟩ → f Walks ⁡ G ⟨“ abc ”⟩
31 wlklenvm1 ⊢ f Walks ⁡ G ⟨“ abc ”⟩ → f = ⟨“ abc ”⟩ − 1
32 simpl ⊢ f = ⟨“ abc ”⟩ − 1 ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f = ⟨“ abc ”⟩ − 1
33 oveq1 ⊢ ⟨“ abc ”⟩ = 2 + 1 → ⟨“ abc ”⟩ − 1 = 2 + 1 - 1
34 2cn ⊢ 2 ∈ ℂ
35 pncan1 ⊢ 2 ∈ ℂ → 2 + 1 - 1 = 2
36 34 35 ax-mp ⊢ 2 + 1 - 1 = 2
37 33 36 eqtrdi ⊢ ⟨“ abc ”⟩ = 2 + 1 → ⟨“ abc ”⟩ − 1 = 2
38 37 adantl ⊢ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 → ⟨“ abc ”⟩ − 1 = 2
39 38 3ad2ant1 ⊢ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → ⟨“ abc ”⟩ − 1 = 2
40 39 adantl ⊢ f = ⟨“ abc ”⟩ − 1 ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → ⟨“ abc ”⟩ − 1 = 2
41 32 40 eqtrd ⊢ f = ⟨“ abc ”⟩ − 1 ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f = 2
42 41 ex ⊢ f = ⟨“ abc ”⟩ − 1 → ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f = 2
43 30 31 42 3syl ⊢ f SPaths ⁡ G ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f = 2
44 43 3ad2ant1 ⊢ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c → ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f = 2
45 44 imp ⊢ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f = 2
46 45 adantl ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ p = ⟨“ abc ”⟩ ∧ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f = 2
47 s3fv0 ⊢ a ∈ V → ⟨“ abc ”⟩ ⁡ 0 = a
48 47 elv ⊢ ⟨“ abc ”⟩ ⁡ 0 = a
49 48 eqcomi ⊢ a = ⟨“ abc ”⟩ ⁡ 0
50 s3fv1 ⊢ b ∈ V → ⟨“ abc ”⟩ ⁡ 1 = b
51 50 elv ⊢ ⟨“ abc ”⟩ ⁡ 1 = b
52 51 eqcomi ⊢ b = ⟨“ abc ”⟩ ⁡ 1
53 s3fv2 ⊢ c ∈ V → ⟨“ abc ”⟩ ⁡ 2 = c
54 53 elv ⊢ ⟨“ abc ”⟩ ⁡ 2 = c
55 54 eqcomi ⊢ c = ⟨“ abc ”⟩ ⁡ 2
56 49 52 55 3pm3.2i ⊢ a = ⟨“ abc ”⟩ ⁡ 0 ∧ b = ⟨“ abc ”⟩ ⁡ 1 ∧ c = ⟨“ abc ”⟩ ⁡ 2
57 56 a1i ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ p = ⟨“ abc ”⟩ ∧ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → a = ⟨“ abc ”⟩ ⁡ 0 ∧ b = ⟨“ abc ”⟩ ⁡ 1 ∧ c = ⟨“ abc ”⟩ ⁡ 2
58 29 46 57 3jca ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ p = ⟨“ abc ”⟩ ∧ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ f = 2 ∧ a = ⟨“ abc ”⟩ ⁡ 0 ∧ b = ⟨“ abc ”⟩ ⁡ 1 ∧ c = ⟨“ abc ”⟩ ⁡ 2
59 breq2 ⊢ p = ⟨“ abc ”⟩ → f SPaths ⁡ G p ↔ f SPaths ⁡ G ⟨“ abc ”⟩
60 fveq1 ⊢ p = ⟨“ abc ”⟩ → p ⁡ 0 = ⟨“ abc ”⟩ ⁡ 0
61 60 eqeq2d ⊢ p = ⟨“ abc ”⟩ → a = p ⁡ 0 ↔ a = ⟨“ abc ”⟩ ⁡ 0
62 fveq1 ⊢ p = ⟨“ abc ”⟩ → p ⁡ 1 = ⟨“ abc ”⟩ ⁡ 1
63 62 eqeq2d ⊢ p = ⟨“ abc ”⟩ → b = p ⁡ 1 ↔ b = ⟨“ abc ”⟩ ⁡ 1
64 fveq1 ⊢ p = ⟨“ abc ”⟩ → p ⁡ 2 = ⟨“ abc ”⟩ ⁡ 2
65 64 eqeq2d ⊢ p = ⟨“ abc ”⟩ → c = p ⁡ 2 ↔ c = ⟨“ abc ”⟩ ⁡ 2
66 61 63 65 3anbi123d ⊢ p = ⟨“ abc ”⟩ → a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ↔ a = ⟨“ abc ”⟩ ⁡ 0 ∧ b = ⟨“ abc ”⟩ ⁡ 1 ∧ c = ⟨“ abc ”⟩ ⁡ 2
67 59 66 3anbi13d ⊢ p = ⟨“ abc ”⟩ → f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ↔ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ f = 2 ∧ a = ⟨“ abc ”⟩ ⁡ 0 ∧ b = ⟨“ abc ”⟩ ⁡ 1 ∧ c = ⟨“ abc ”⟩ ⁡ 2
68 67 ad2antlr ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ p = ⟨“ abc ”⟩ ∧ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ↔ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ f = 2 ∧ a = ⟨“ abc ”⟩ ⁡ 0 ∧ b = ⟨“ abc ”⟩ ⁡ 1 ∧ c = ⟨“ abc ”⟩ ⁡ 2
69 58 68 mpbird ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ p = ⟨“ abc ”⟩ ∧ f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
70 69 ex ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ p = ⟨“ abc ”⟩ → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
71 28 70 spcimedv ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c → ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
72 spthiswlk ⊢ f SPaths ⁡ G p → f Walks ⁡ G p
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 eqeq2d ⊢ f = 2 → p = f + 1 ↔ p = 3
78 77 biimpcd ⊢ p = f + 1 → f = 2 → p = 3
79 72 73 78 3syl ⊢ f SPaths ⁡ G p → f = 2 → p = 3
80 79 imp ⊢ f SPaths ⁡ G p ∧ f = 2 → p = 3
81 80 3adant3 ⊢ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p = 3
82 81 adantl ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p = 3
83 eqcom ⊢ a = p ⁡ 0 ↔ p ⁡ 0 = a
84 eqcom ⊢ b = p ⁡ 1 ↔ p ⁡ 1 = b
85 eqcom ⊢ c = p ⁡ 2 ↔ p ⁡ 2 = c
86 83 84 85 3anbi123i ⊢ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ↔ p ⁡ 0 = a ∧ p ⁡ 1 = b ∧ p ⁡ 2 = c
87 86 biimpi ⊢ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p ⁡ 0 = a ∧ p ⁡ 1 = b ∧ p ⁡ 2 = c
88 87 3ad2ant3 ⊢ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p ⁡ 0 = a ∧ p ⁡ 1 = b ∧ p ⁡ 2 = c
89 88 adantl ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p ⁡ 0 = a ∧ p ⁡ 1 = b ∧ p ⁡ 2 = c
90 82 89 jca ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ 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 72 91 syl ⊢ f SPaths ⁡ G p → p ∈ Word V
93 92 3ad2ant1 ⊢ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p ∈ Word V
94 12 anim1i ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → a ∈ V ∧ b ∈ V ∧ c ∈ V
95 3anass ⊢ a ∈ V ∧ b ∈ V ∧ c ∈ V ↔ a ∈ V ∧ b ∈ V ∧ c ∈ V
96 94 95 sylibr ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → a ∈ V ∧ b ∈ V ∧ c ∈ V
97 eqwrds3 ⊢ p ∈ Word V ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → p = ⟨“ abc ”⟩ ↔ p = 3 ∧ p ⁡ 0 = a ∧ p ⁡ 1 = b ∧ p ⁡ 2 = c
98 93 96 97 syl2anr ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ 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
99 90 98 mpbird ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p = ⟨“ abc ”⟩
100 59 biimpcd ⊢ f SPaths ⁡ G p → p = ⟨“ abc ”⟩ → f SPaths ⁡ G ⟨“ abc ”⟩
101 100 3ad2ant1 ⊢ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p = ⟨“ abc ”⟩ → f SPaths ⁡ G ⟨“ abc ”⟩
102 101 adantl ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p = ⟨“ abc ”⟩ → f SPaths ⁡ G ⟨“ abc ”⟩
103 102 imp ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → f SPaths ⁡ G ⟨“ abc ”⟩
104 48 a1i ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ⁡ 0 = a
105 fveq2 ⊢ f = 2 → ⟨“ abc ”⟩ ⁡ f = ⟨“ abc ”⟩ ⁡ 2
106 105 54 eqtrdi ⊢ f = 2 → ⟨“ abc ”⟩ ⁡ f = c
107 106 3ad2ant2 ⊢ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → ⟨“ abc ”⟩ ⁡ f = c
108 107 ad2antlr ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ⁡ f = c
109 103 104 108 3jca ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c
110 wlkiswwlks1 ⊢ G ∈ UPGraph → f Walks ⁡ G p → p ∈ WWalks ⁡ G
111 110 adantr ⊢ G ∈ UPGraph ∧ a ∈ V → f Walks ⁡ G p → p ∈ WWalks ⁡ G
112 111 adantr ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → f Walks ⁡ G p → p ∈ WWalks ⁡ G
113 72 112 syl5com ⊢ f SPaths ⁡ G p → G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → p ∈ WWalks ⁡ G
114 113 3ad2ant1 ⊢ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → p ∈ WWalks ⁡ G
115 114 impcom ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → p ∈ WWalks ⁡ G
116 115 adantr ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → p ∈ WWalks ⁡ G
117 eleq1 ⊢ p = ⟨“ abc ”⟩ → p ∈ WWalks ⁡ G ↔ ⟨“ abc ”⟩ ∈ WWalks ⁡ G
118 117 bicomd ⊢ p = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ∈ WWalks ⁡ G ↔ p ∈ WWalks ⁡ G
119 118 adantl ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ∈ WWalks ⁡ G ↔ p ∈ WWalks ⁡ G
120 116 119 mpbird ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ∈ WWalks ⁡ G
121 s3len ⊢ ⟨“ abc ”⟩ = 3
122 df-3 ⊢ 3 = 2 + 1
123 121 122 eqtri ⊢ ⟨“ abc ”⟩ = 2 + 1
124 120 123 jctir ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1
125 54 a1i ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ⁡ 2 = c
126 124 104 125 3jca ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
127 109 126 jca ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 ∧ p = ⟨“ abc ”⟩ → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
128 99 127 mpdan ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
129 128 ex ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
130 129 exlimdv ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2 → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c
131 71 130 impbid ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c ↔ ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
132 131 adantr ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ W = ⟨“ abc ”⟩ → f SPaths ⁡ G ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ f = c ∧ ⟨“ abc ”⟩ ∈ WWalks ⁡ G ∧ ⟨“ abc ”⟩ = 2 + 1 ∧ ⟨“ abc ”⟩ ⁡ 0 = a ∧ ⟨“ abc ”⟩ ⁡ 2 = c ↔ ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
133 27 132 bitrd ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ W = ⟨“ abc ”⟩ → f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ↔ ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
134 133 exbidv ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ W = ⟨“ abc ”⟩ → ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ↔ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
135 11 134 bitrid ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ W = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ∈ a 2 WWalksNOn G c ∧ ∃ f f a SPathsOn ⁡ G c ⟨“ abc ”⟩ ↔ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
136 8 135 bitrid ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ W = ⟨“ abc ”⟩ → ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c ↔ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
137 136 pm5.32da ⊢ G ∈ UPGraph ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V → W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c ↔ W = ⟨“ abc ”⟩ ∧ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
138 137 2rexbidva ⊢ G ∈ UPGraph ∧ a ∈ V → ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c ↔ ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ ∧ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
139 7 138 bitrid ⊢ G ∈ UPGraph ∧ a ∈ V → ∃ c ∈ V ∃ b ∈ V W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c ↔ ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ ∧ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
140 139 rexbidva ⊢ G ∈ UPGraph → ∃ a ∈ V ∃ c ∈ V ∃ b ∈ V W = ⟨“ abc ”⟩ ∧ ⟨“ abc ”⟩ ∈ a 2 WSPathsNOn G c ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ ∧ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2
141 3 6 140 3bitrd ⊢ G ∈ UPGraph → W ∈ 2 WSPathsN G ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ ∧ ∃ f ∃ p f SPaths ⁡ G p ∧ f = 2 ∧ a = p ⁡ 0 ∧ b = p ⁡ 1 ∧ c = p ⁡ 2