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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	usgrcyclgt2v	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 2 < ( ♯ ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		usgrcyclgt2v.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		2re	⊢ 2 ∈ ℝ
3	2	rexri	⊢ 2 ∈ ℝ*
4	3	a1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 2 ∈ ℝ* )
5		cycliswlk	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
6		wlkcl	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
7		nn0xnn0	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℕ0* )
8		xnn0xr	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0* → ( ♯ ‘ 𝐹 ) ∈ ℝ* )
9	5 6 7 8	4syl	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℝ* )
10	9	3ad2ant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ∈ ℝ* )
11	1	fvexi	⊢ 𝑉 ∈ V
12		hashxnn0	⊢ ( 𝑉 ∈ V → ( ♯ ‘ 𝑉 ) ∈ ℕ0* )
13		xnn0xr	⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0* → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
14	11 12 13	mp2b	⊢ ( ♯ ‘ 𝑉 ) ∈ ℝ*
15	14	a1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
16		usgrgt2cycl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 2 < ( ♯ ‘ 𝐹 ) )
17		cyclispth	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
18	1	pthhashvtx	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )
19	17 18	syl	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )
20	19	3ad2ant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )
21	4 10 15 16 20	xrltletrd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 2 < ( ♯ ‘ 𝑉 ) )