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 )