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 nn0xnn0 ⊢ F ∈ ℕ 0 → F ∈ ℕ 0 *
8 xnn0xr ⊢ F ∈ ℕ 0 * → F ∈ ℝ *
9 5 6 7 8 4syl ⊢ F Cycles ⁡ G P → F ∈ ℝ *
10 9 3ad2ant2 ⊢ G ∈ USGraph ∧ F Cycles ⁡ G P ∧ F ≠ ∅ → F ∈ ℝ *
11 1 fvexi ⊢ V ∈ V
12 hashxnn0 ⊢ V ∈ V → V ∈ ℕ 0 *
13 xnn0xr ⊢ V ∈ ℕ 0 * → V ∈ ℝ *
14 11 12 13 mp2b ⊢ V ∈ ℝ *
15 14 a1i ⊢ G ∈ USGraph ∧ F Cycles ⁡ G P ∧ F ≠ ∅ → V ∈ ℝ *
16 usgrgt2cycl ⊢ G ∈ 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 ∈ USGraph ∧ F Cycles ⁡ G P ∧ F ≠ ∅ → F ≤ V
21 4 10 15 16 20 xrltletrd ⊢ G ∈ USGraph ∧ F Cycles ⁡ G P ∧ F ≠ ∅ → 2 < V