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