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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion elwspths2spth ( 𝐺 ∈ UPGraph → ( 𝑊 ∈ ( 2 WSPathsN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) ) )

Proof

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