Description: In a simple graph there are no cycles with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017) (Revised by AV, 4-Feb-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | usgrn2cycl | |- ( ( G e. USGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 2 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | usgruspgr | |- ( G e. USGraph -> G e. USPGraph ) |
|
| 2 | cycliscrct | |- ( F ( Cycles ` G ) P -> F ( Circuits ` G ) P ) |
|
| 3 | uspgrn2crct | |- ( ( G e. USPGraph /\ F ( Circuits ` G ) P ) -> ( # ` F ) =/= 2 ) |
|
| 4 | 1 2 3 | syl2an | |- ( ( G e. USGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 2 ) |