Metamath Proof Explorer

Theorem usgrcyclgt2v

Description: A simple graph with a non-trivial cycle must have at least 3 vertices. (Contributed by BTernaryTau, 5-Oct-2023)

Ref Expression
Hypothesis usgrcyclgt2v.1 
|- V = ( Vtx ` G )
Assertion usgrcyclgt2v 
|- ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 2 < ( # ` V ) )

Proof

Step Hyp Ref Expression
1 usgrcyclgt2v.1 
 |-  V = ( Vtx ` G )
2 2re 
 |-  2 e. RR
3 2 rexri 
 |-  2 e. RR*
4 3 a1i 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 2 e. RR* )
5 cycliswlk 
 |-  ( F ( Cycles ` G ) P -> F ( Walks ` G ) P )
6 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
7 5 6 syl 
 |-  ( F ( Cycles ` G ) P -> ( # ` F ) e. NN0 )
8 nn0xnn0 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. NN0* )
9 xnn0xr 
 |-  ( ( # ` F ) e. NN0* -> ( # ` F ) e. RR* )
10 7 8 9 3syl 
 |-  ( F ( Cycles ` G ) P -> ( # ` F ) e. RR* )
11 10 3ad2ant2 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` F ) e. RR* )
12 1 fvexi 
 |-  V e. _V
13 hashxnn0 
 |-  ( V e. _V -> ( # ` V ) e. NN0* )
14 xnn0xr 
 |-  ( ( # ` V ) e. NN0* -> ( # ` V ) e. RR* )
15 12 13 14 mp2b 
 |-  ( # ` V ) e. RR*
16 15 a1i 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` V ) e. RR* )
17 usgrgt2cycl 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 2 < ( # ` F ) )
18 cyclispth 
 |-  ( F ( Cycles ` G ) P -> F ( Paths ` G ) P )
19 1 pthhashvtx 
 |-  ( F ( Paths ` G ) P -> ( # ` F ) <_ ( # ` V ) )
20 18 19 syl 
 |-  ( F ( Cycles ` G ) P -> ( # ` F ) <_ ( # ` V ) )
21 20 3ad2ant2 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` F ) <_ ( # ` V ) )
22 4 11 16 17 21 xrltletrd 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 2 < ( # ` V ) )