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 ) ) ) )