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 nn0xnn0 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. NN0* )
8 xnn0xr 
 |-  ( ( # ` F ) e. NN0* -> ( # ` F ) e. RR* )
9 5 6 7 8 4syl 
 |-  ( F ( Cycles ` G ) P -> ( # ` F ) e. RR* )
10 9 3ad2ant2 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` F ) e. RR* )
11 1 fvexi 
 |-  V e. _V
12 hashxnn0 
 |-  ( V e. _V -> ( # ` V ) e. NN0* )
13 xnn0xr 
 |-  ( ( # ` V ) e. NN0* -> ( # ` V ) e. RR* )
14 11 12 13 mp2b 
 |-  ( # ` V ) e. RR*
15 14 a1i 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` V ) e. RR* )
16 usgrgt2cycl 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 2 < ( # ` F ) )
17 cyclispth 
 |-  ( F ( Cycles ` G ) P -> F ( Paths ` G ) P )
18 1 pthhashvtx 
 |-  ( F ( Paths ` G ) P -> ( # ` F ) <_ ( # ` V ) )
19 17 18 syl 
 |-  ( F ( Cycles ` G ) P -> ( # ` F ) <_ ( # ` V ) )
20 19 3ad2ant2 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` F ) <_ ( # ` V ) )
21 4 10 15 16 20 xrltletrd 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 2 < ( # ` V ) )