This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrwwlks2on

Description: A walk of length 2 between two vertices as word in a simple graph. This theorem is analogous to umgrwwlks2on except it talks about simple graphs and therefore does not require the Axiom of Choice for its proof. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses s3wwlks2on.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
usgrwwlks2on.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion usgrwwlks2on ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 s3wwlks2on.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgrwwlks2on.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 usgruspgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
4 3 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐺 ∈ USPGraph )
5 simpr1 ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
6 simpr3 ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
7 1 sps3wwlks2on ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
8 4 5 6 7 syl3anc ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
9 usgrupgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
10 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
11 1 10 upgr2wlk ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } ) ) ) )
12 9 11 syl ⊢ ( 𝐺 ∈ USGraph → ( ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } ) ) ) )
13 12 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } ) ) ) )
14 s3fv0 ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
15 14 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
16 s3fv1 ⊢ ( 𝐵 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
17 16 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
18 15 17 preq12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } = { 𝐴 , 𝐵 } )
19 18 eqeq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ) )
20 s3fv2 ⊢ ( 𝐶 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
21 20 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
22 17 21 preq12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } = { 𝐵 , 𝐶 } )
23 22 eqeq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) )
24 19 23 anbi12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } ) ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) )
25 24 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } ) ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) )
26 25 3anbi3d ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } ) ) ↔ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) )
27 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
28 10 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
29 fdmrn ⊢ ( Fun ( iEdg ‘ 𝐺 ) ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) )
30 simpr ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) )
31 id ⊢ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) → 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) )
32 c0ex ⊢ 0 ∈ V
33 32 prid1 ⊢ 0 ∈ { 0 , 1 }
34 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
35 33 34 eleqtrri ⊢ 0 ∈ ( 0 ..^ 2 )
36 35 a1i ⊢ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) → 0 ∈ ( 0 ..^ 2 ) )
37 31 36 ffvelcdmd ⊢ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( 𝑓 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) )
38 37 adantr ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) ) → ( 𝑓 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) )
39 30 38 ffvelcdmd ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) )
40 1ex ⊢ 1 ∈ V
41 40 prid2 ⊢ 1 ∈ { 0 , 1 }
42 41 34 eleqtrri ⊢ 1 ∈ ( 0 ..^ 2 )
43 42 a1i ⊢ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) → 1 ∈ ( 0 ..^ 2 ) )
44 31 43 ffvelcdmd ⊢ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( 𝑓 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) )
45 44 adantr ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) ) → ( 𝑓 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) )
46 30 45 ffvelcdmd ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) )
47 39 46 jca ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) )
48 47 ex ⊢ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) ) )
49 48 3ad2ant1 ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) ) )
50 49 com12 ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ran ( iEdg ‘ 𝐺 ) → ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) ) )
51 29 50 sylbi ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) ) )
52 27 28 51 3syl ⊢ ( 𝐺 ∈ USGraph → ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) ) )
53 52 imp ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) )
54 eqcom ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) )
55 54 biimpi ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } → { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) )
56 55 adantr ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) → { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) )
57 56 3ad2ant3 ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) → { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) )
58 57 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) → { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) )
59 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
60 2 59 eqtri ⊢ 𝐸 = ran ( iEdg ‘ 𝐺 )
61 60 a1i ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) → 𝐸 = ran ( iEdg ‘ 𝐺 ) )
62 58 61 eleq12d ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) )
63 eqcom ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ↔ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) )
64 63 biimpi ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } → { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) )
65 64 adantl ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) → { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) )
66 65 3ad2ant3 ⊢ ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) → { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) )
67 66 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) → { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) )
68 67 61 eleq12d ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) → ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) )
69 62 68 anbi12d ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) ) )
70 53 69 mpbird ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
71 70 ex ⊢ ( 𝐺 ∈ USGraph → ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
72 71 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { 𝐴 , 𝐵 } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { 𝐵 , 𝐶 } ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
73 26 72 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑓 : ( 0 ..^ 2 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 0 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 1 ) ) = { ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) , ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) } ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
74 13 73 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
75 74 exlimdv ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
76 usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
77 76 3ad2ant1 ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐺 ∈ UMGraph )
78 simp2 ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → { 𝐴 , 𝐵 } ∈ 𝐸 )
79 simp3 ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → { 𝐵 , 𝐶 } ∈ 𝐸 )
80 2 umgr2wlk ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) )
81 77 78 79 80 syl3anc ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) )
82 wlklenvp1 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) )
83 oveq1 ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( ( ♯ ‘ 𝑓 ) + 1 ) = ( 2 + 1 ) )
84 2p1e3 ⊢ ( 2 + 1 ) = 3
85 83 84 eqtrdi ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( ( ♯ ‘ 𝑓 ) + 1 ) = 3 )
86 85 adantr ⊢ ( ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( ( ♯ ‘ 𝑓 ) + 1 ) = 3 )
87 82 86 sylan9eq ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( ♯ ‘ 𝑝 ) = 3 )
88 eqcom ⊢ ( 𝐴 = ( 𝑝 ‘ 0 ) ↔ ( 𝑝 ‘ 0 ) = 𝐴 )
89 eqcom ⊢ ( 𝐵 = ( 𝑝 ‘ 1 ) ↔ ( 𝑝 ‘ 1 ) = 𝐵 )
90 eqcom ⊢ ( 𝐶 = ( 𝑝 ‘ 2 ) ↔ ( 𝑝 ‘ 2 ) = 𝐶 )
91 88 89 90 3anbi123i ⊢ ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ↔ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 1 ) = 𝐵 ∧ ( 𝑝 ‘ 2 ) = 𝐶 ) )
92 91 biimpi ⊢ ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 1 ) = 𝐵 ∧ ( 𝑝 ‘ 2 ) = 𝐶 ) )
93 92 adantl ⊢ ( ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 1 ) = 𝐵 ∧ ( 𝑝 ‘ 2 ) = 𝐶 ) )
94 93 adantl ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 1 ) = 𝐵 ∧ ( 𝑝 ‘ 2 ) = 𝐶 ) )
95 87 94 jca ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( ( ♯ ‘ 𝑝 ) = 3 ∧ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 1 ) = 𝐵 ∧ ( 𝑝 ‘ 2 ) = 𝐶 ) ) )
96 1 wlkpwrd ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → 𝑝 ∈ Word 𝑉 )
97 85 eqeq2d ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ↔ ( ♯ ‘ 𝑝 ) = 3 ) )
98 97 adantl ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ↔ ( ♯ ‘ 𝑝 ) = 3 ) )
99 simp1 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 3 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → 𝑝 ∈ Word 𝑉 )
100 oveq2 ⊢ ( ( ♯ ‘ 𝑝 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = ( 0 ..^ 3 ) )
101 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
102 100 101 eqtrdi ⊢ ( ( ♯ ‘ 𝑝 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } )
103 32 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
104 eleq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) ↔ 0 ∈ { 0 , 1 , 2 } ) )
105 103 104 mpbiri ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) )
106 wrdsymbcl ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) ) → ( 𝑝 ‘ 0 ) ∈ 𝑉 )
107 105 106 sylan2 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } ) → ( 𝑝 ‘ 0 ) ∈ 𝑉 )
108 40 tpid2 ⊢ 1 ∈ { 0 , 1 , 2 }
109 eleq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } → ( 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) ↔ 1 ∈ { 0 , 1 , 2 } ) )
110 108 109 mpbiri ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) )
111 wrdsymbcl ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) ) → ( 𝑝 ‘ 1 ) ∈ 𝑉 )
112 110 111 sylan2 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } ) → ( 𝑝 ‘ 1 ) ∈ 𝑉 )
113 2ex ⊢ 2 ∈ V
114 113 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
115 eleq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } → ( 2 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) ↔ 2 ∈ { 0 , 1 , 2 } ) )
116 114 115 mpbiri ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } → 2 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) )
117 wrdsymbcl ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) ) → ( 𝑝 ‘ 2 ) ∈ 𝑉 )
118 116 117 sylan2 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } ) → ( 𝑝 ‘ 2 ) ∈ 𝑉 )
119 107 112 118 3jca ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( 0 ..^ ( ♯ ‘ 𝑝 ) ) = { 0 , 1 , 2 } ) → ( ( 𝑝 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 2 ) ∈ 𝑉 ) )
120 102 119 sylan2 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 3 ) → ( ( 𝑝 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 2 ) ∈ 𝑉 ) )
121 120 3adant3 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 3 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( ( 𝑝 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 2 ) ∈ 𝑉 ) )
122 eleq1 ⊢ ( 𝐴 = ( 𝑝 ‘ 0 ) → ( 𝐴 ∈ 𝑉 ↔ ( 𝑝 ‘ 0 ) ∈ 𝑉 ) )
123 122 3ad2ant1 ⊢ ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝐴 ∈ 𝑉 ↔ ( 𝑝 ‘ 0 ) ∈ 𝑉 ) )
124 eleq1 ⊢ ( 𝐵 = ( 𝑝 ‘ 1 ) → ( 𝐵 ∈ 𝑉 ↔ ( 𝑝 ‘ 1 ) ∈ 𝑉 ) )
125 124 3ad2ant2 ⊢ ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝐵 ∈ 𝑉 ↔ ( 𝑝 ‘ 1 ) ∈ 𝑉 ) )
126 eleq1 ⊢ ( 𝐶 = ( 𝑝 ‘ 2 ) → ( 𝐶 ∈ 𝑉 ↔ ( 𝑝 ‘ 2 ) ∈ 𝑉 ) )
127 126 3ad2ant3 ⊢ ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝐶 ∈ 𝑉 ↔ ( 𝑝 ‘ 2 ) ∈ 𝑉 ) )
128 123 125 127 3anbi123d ⊢ ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( ( 𝑝 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 2 ) ∈ 𝑉 ) ) )
129 128 3ad2ant3 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 3 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( ( 𝑝 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑝 ‘ 2 ) ∈ 𝑉 ) ) )
130 121 129 mpbird ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 3 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
131 99 130 jca ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 3 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) )
132 131 3exp ⊢ ( 𝑝 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑝 ) = 3 → ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ) ) )
133 132 adantr ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( ♯ ‘ 𝑝 ) = 3 → ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ) ) )
134 98 133 sylbid ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) → ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ) ) )
135 134 impancom ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ( ♯ ‘ 𝑓 ) = 2 → ( ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ) ) )
136 135 impd ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ) → ( ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ) )
137 96 82 136 syl2anc ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ) )
138 137 imp ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) )
139 eqwrds3 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( ♯ ‘ 𝑝 ) = 3 ∧ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 1 ) = 𝐵 ∧ ( 𝑝 ‘ 2 ) = 𝐶 ) ) ) )
140 138 139 syl ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( ♯ ‘ 𝑝 ) = 3 ∧ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 1 ) = 𝐵 ∧ ( 𝑝 ‘ 2 ) = 𝐶 ) ) ) )
141 95 140 mpbird ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → 𝑝 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
142 141 breq2d ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) )
143 142 biimpd ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) )
144 143 ex ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) )
145 144 pm2.43a ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) )
146 145 3impib ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
147 146 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
148 simpr2 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( ♯ ‘ 𝑓 ) = 2 )
149 147 148 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
150 149 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
151 150 exlimdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
152 151 eximdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝐴 = ( 𝑝 ‘ 0 ) ∧ 𝐵 = ( 𝑝 ‘ 1 ) ∧ 𝐶 = ( 𝑝 ‘ 2 ) ) ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
153 81 152 syl5com ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
154 153 3expib ⊢ ( 𝐺 ∈ USGraph → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) )
155 154 com23 ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) )
156 155 imp ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
157 75 156 impbid ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
158 8 157 bitrd ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )