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 
|- ( ( G e. USPGraph /\ F ( Circuits ` G ) P ) -> ( # ` F ) =/= 2 )

Proof

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