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 USGraph F Cycles G P F 2 < V

Proof

Step Hyp Ref Expression
1 usgrcyclgt2v.1 V = Vtx G
2 2re 2
3 2 rexri 2 *
4 3 a1i G USGraph F Cycles G P F 2 *
5 cycliswlk F Cycles G P F Walks G P
6 wlkcl F Walks G P F 0
7 5 6 syl F Cycles G P F 0
8 nn0xnn0 F 0 F 0 *
9 xnn0xr F 0 * F *
10 7 8 9 3syl F Cycles G P F *
11 10 3ad2ant2 G USGraph F Cycles G P F F *
12 1 fvexi V V
13 hashxnn0 V V V 0 *
14 xnn0xr V 0 * V *
15 12 13 14 mp2b V *
16 15 a1i G USGraph F Cycles G P F V *
17 usgrgt2cycl G 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 USGraph F Cycles G P F F V
22 4 11 16 17 21 xrltletrd G USGraph F Cycles G P F 2 < V