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

Metamath Proof Explorer

Theorem usgr2trlncl

Description: In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Assertion usgr2trlncl ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )

Proof

Step Hyp Ref Expression
1 usgrupgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4 2 3 upgrf1istrl ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
5 1 4 syl ⊢ ( 𝐺 ∈ USGraph → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
6 eqidd ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → 𝐹 = 𝐹 )
7 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) )
8 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
9 7 8 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } )
10 eqidd ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 ) )
11 6 9 10 f1eq123d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ↔ 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ) )
12 9 raleqdv ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ { 0 , 1 } ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
13 2wlklem ⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
14 12 13 bitrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) )
15 11 14 anbi12d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
16 15 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
17 c0ex ⊢ 0 ∈ V
18 1ex ⊢ 1 ∈ V
19 17 18 pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V )
20 0ne1 ⊢ 0 ≠ 1
21 eqid ⊢ { 0 , 1 } = { 0 , 1 }
22 21 f12dfv ⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ 0 ≠ 1 ) → ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ↔ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) ) )
23 19 20 22 mp2an ⊢ ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ↔ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) )
24 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
25 3 24 usgrf1oedg ⊢ ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) )
26 f1of1 ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) )
27 id ⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) )
28 17 prid1 ⊢ 0 ∈ { 0 , 1 }
29 28 a1i ⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → 0 ∈ { 0 , 1 } )
30 27 29 ffvelcdmd ⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → ( 𝐹 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) )
31 18 prid2 ⊢ 1 ∈ { 0 , 1 }
32 31 a1i ⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → 1 ∈ { 0 , 1 } )
33 27 32 ffvelcdmd ⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → ( 𝐹 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) )
34 30 33 jca ⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → ( ( 𝐹 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
35 34 anim1ci ⊢ ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ∧ ( ( 𝐹 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
36 f1veqaeq ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ∧ ( ( 𝐹 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) ) )
37 35 36 syl ⊢ ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) ) )
38 37 necon3d ⊢ ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) ) )
39 simpl ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
40 simpr ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
41 39 40 neeq12d ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
42 preq1 ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } )
43 prcom ⊢ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) }
44 42 43 eqtrdi ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
45 44 necon3i ⊢ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) )
46 41 45 biimtrdi ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
47 46 com12 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
48 47 a1d ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝐺 ∈ USGraph → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
49 38 48 syl6 ⊢ ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) → ( 𝐺 ∈ USGraph → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
50 49 expcom ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) → ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) → ( 𝐺 ∈ USGraph → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) ) )
51 50 impd ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) → ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( 𝐺 ∈ USGraph → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
52 51 com23 ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) → ( 𝐺 ∈ USGraph → ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
53 26 52 syl ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) → ( 𝐺 ∈ USGraph → ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) )
54 25 53 mpcom ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
55 23 54 biimtrid ⊢ ( 𝐺 ∈ USGraph → ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
56 55 impd ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
57 56 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
58 16 57 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
59 58 com12 ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
60 59 3adant2 ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
61 60 expdcom ⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
62 61 com23 ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
63 5 62 sylbid ⊢ ( 𝐺 ∈ USGraph → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
64 63 com23 ⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
65 64 imp ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )