# Metamath Proof Explorer

## Theorem umgr2wlk

Description: In a multigraph, there is a walk of length 2 for each pair of adjacent edges. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 30-Jan-2021)

Ref Expression
Hypothesis umgr2wlk.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgr2wlk ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) )

### Proof

Step Hyp Ref Expression
1 umgr2wlk.e 𝐸 = ( Edg ‘ 𝐺 )
2 umgruhgr ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
3 1 eleq2i ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) )
4 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5 4 uhgredgiedgb ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
6 3 5 syl5bb ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
7 2 6 syl ( 𝐺 ∈ UMGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
8 7 biimpd ( 𝐺 ∈ UMGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸 → ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
9 8 a1d ( 𝐺 ∈ UMGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( { 𝐵 , 𝐶 } ∈ 𝐸 → ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
10 9 3imp ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
11 1 eleq2i ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
12 4 uhgredgiedgb ( 𝐺 ∈ UHGraph → ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
13 11 12 syl5bb ( 𝐺 ∈ UHGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
14 2 13 syl ( 𝐺 ∈ UMGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
15 14 biimpd ( 𝐺 ∈ UMGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
16 15 a1dd ( 𝐺 ∈ UMGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( { 𝐵 , 𝐶 } ∈ 𝐸 → ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) )
17 16 3imp ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) )
18 s2cli ⟨“ 𝑗 𝑖 ”⟩ ∈ Word V
19 s3cli ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V
20 18 19 pm3.2i ( ⟨“ 𝑗 𝑖 ”⟩ ∈ Word V ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V )
21 eqid ⟨“ 𝑗 𝑖 ”⟩ = ⟨“ 𝑗 𝑖 ”⟩
22 eqid ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐴 𝐵 𝐶 ”⟩
23 simpl1 ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → 𝐺 ∈ UMGraph )
24 3simpc ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
25 24 adantr ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
26 simpl ( ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) )
27 26 eqcomd ( ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐴 , 𝐵 } )
28 27 adantl ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = { 𝐴 , 𝐵 } )
29 simpr ( ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
30 29 eqcomd ( ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐵 , 𝐶 } )
31 30 adantl ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐵 , 𝐶 } )
32 1 4 21 22 23 25 28 31 umgr2adedgwlk ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ⟨“ 𝑗 𝑖 ”⟩ ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑗 𝑖 ”⟩ ) = 2 ∧ ( 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ∧ 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) )
33 breq12 ( ( 𝑓 = ⟨“ 𝑗 𝑖 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ ⟨“ 𝑗 𝑖 ”⟩ ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) )
34 fveqeq2 ( 𝑓 = ⟨“ 𝑗 𝑖 ”⟩ → ( ( ♯ ‘ 𝑓 ) = 2 ↔ ( ♯ ‘ ⟨“ 𝑗 𝑖 ”⟩ ) = 2 ) )
35 34 adantr ( ( 𝑓 = ⟨“ 𝑗 𝑖 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( ♯ ‘ 𝑓 ) = 2 ↔ ( ♯ ‘ ⟨“ 𝑗 𝑖 ”⟩ ) = 2 ) )
36 fveq1 ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) )
37 36 eqeq2d ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝐴 = ( 𝑝 ‘ 0 ) ↔ 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ) )
38 fveq1 ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑝 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
39 38 eqeq2d ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝐵 = ( 𝑝 ‘ 1 ) ↔ 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
40 fveq1 ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝑝 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
41 40 eqeq2d ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( 𝐶 = ( 𝑝 ‘ 2 ) ↔ 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) )
42 37 39 41 3anbi123d ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ → ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ↔ ( 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ∧ 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) )
43 42 adantl ( ( 𝑓 = ⟨“ 𝑗 𝑖 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ↔ ( 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ∧ 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) )
44 33 35 43 3anbi123d ( ( 𝑓 = ⟨“ 𝑗 𝑖 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ↔ ( ⟨“ 𝑗 𝑖 ”⟩ ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑗 𝑖 ”⟩ ) = 2 ∧ ( 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ∧ 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) ) )
45 44 spc2egv ( ( ⟨“ 𝑗 𝑖 ”⟩ ∈ Word V ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V ) → ( ( ⟨“ 𝑗 𝑖 ”⟩ ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑗 𝑖 ”⟩ ) = 2 ∧ ( 𝐴 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ∧ 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝐶 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) )
46 20 32 45 mpsyl ( ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) )
47 46 exp32 ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) ) )
48 47 com12 ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) ) )
49 48 rexlimivw ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) ) )
50 49 com13 ( { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) ) )
51 50 rexlimivw ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) ) )
52 51 com12 ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) ) )
53 10 17 52 mp2d ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) )