Metamath Proof Explorer

Theorem uspgrn2crct

Description: In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017) (Revised by AV, 3-Feb-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Assertion uspgrn2crct ( ( 𝐺 ∈ USPGraph ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 2 )

Proof

Step Hyp Ref Expression
1 crctprop ⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
2 istrl ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) )
3 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 4 5 upgriswlk ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
7 preq2 ⊢ ( ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } )
8 prcom ⊢ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) }
9 7 8 eqtrdi ⊢ ( ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
10 9 eqcoms ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
11 10 eqeq2d ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
12 11 anbi2d ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) )
13 12 ad2antrr ⊢ ( ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) )
14 eqtr3 ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) )
15 4 5 uspgrf ⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
16 15 adantl ⊢ ( ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
17 16 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
18 17 adantr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
19 df-f1 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ Fun ◡ 𝐹 ) )
20 19 simplbi2 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( Fun ◡ 𝐹 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) )
21 wrdf ⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) )
22 20 21 syl11 ⊢ ( Fun ◡ 𝐹 → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) )
23 22 adantr ⊢ ( ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) )
24 23 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) )
25 24 imp ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) )
26 2nn ⊢ 2 ∈ ℕ
27 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ 2 ∈ ℕ )
28 26 27 mpbir ⊢ 0 ∈ ( 0 ..^ 2 )
29 1nn0 ⊢ 1 ∈ ℕ0
30 1lt2 ⊢ 1 < 2
31 elfzo0 ⊢ ( 1 ∈ ( 0 ..^ 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2 ) )
32 29 26 30 31 mpbir3an ⊢ 1 ∈ ( 0 ..^ 2 )
33 28 32 pm3.2i ⊢ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) )
34 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) )
35 34 eleq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 0 ∈ ( 0 ..^ 2 ) ) )
36 34 eleq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 1 ∈ ( 0 ..^ 2 ) ) )
37 35 36 anbi12d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) ) )
38 33 37 mpbiri ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
39 38 ad2antrr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
40 f1cofveqaeq ⊢ ( ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) ∧ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → 0 = 1 ) )
41 18 25 39 40 syl21anc ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → 0 = 1 ) )
42 0ne1 ⊢ 0 ≠ 1
43 eqneqall ⊢ ( 0 = 1 → ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
44 41 42 43 syl6mpi ⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
45 44 adantll ⊢ ( ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
46 14 45 syl5 ⊢ ( ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
47 13 46 sylbid ⊢ ( ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
48 47 expimpd ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
49 48 ex ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
50 2a1 ⊢ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) → ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
51 49 50 pm2.61ine ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
52 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
53 34 52 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } )
54 53 raleqdv ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ∀ 𝑘 ∈ { 0 , 1 } ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
55 2wlklem ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
56 54 55 bitrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) )
57 56 anbi2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
58 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 2 ) )
59 58 neeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
60 57 59 imbi12d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
61 60 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
62 51 61 mpbird ⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
63 62 ex ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
64 63 com13 ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
65 64 expd ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( Fun ◡ 𝐹 → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) )
66 65 3adant2 ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( Fun ◡ 𝐹 → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) )
67 6 66 syl6bi ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( Fun ◡ 𝐹 → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) ) )
68 67 impd ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) )
69 68 com23 ⊢ ( 𝐺 ∈ UPGraph → ( 𝐺 ∈ USPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) )
70 3 69 mpcom ⊢ ( 𝐺 ∈ USPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
71 70 com12 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
72 2 71 sylbi ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
73 72 imp ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐺 ∈ USPGraph ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
74 73 necon2d ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐺 ∈ USPGraph ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ≠ 2 ) )
75 74 impancom ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐺 ∈ USPGraph → ( ♯ ‘ 𝐹 ) ≠ 2 ) )
76 1 75 syl ⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ USPGraph → ( ♯ ‘ 𝐹 ) ≠ 2 ) )
77 76 impcom ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 2 )