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	5 6	syl	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
8		nn0xnn0	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℕ0* )
9		xnn0xr	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0* → ( ♯ ‘ 𝐹 ) ∈ ℝ* )
10	7 8 9	3syl	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℝ* )
11	10	3ad2ant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ∈ ℝ* )
12	1	fvexi	⊢ 𝑉 ∈ V
13		hashxnn0	⊢ ( 𝑉 ∈ V → ( ♯ ‘ 𝑉 ) ∈ ℕ0* )
14		xnn0xr	⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0* → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
15	12 13 14	mp2b	⊢ ( ♯ ‘ 𝑉 ) ∈ ℝ*
16	15	a1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
17		usgrgt2cycl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 2 < ( ♯ ‘ 𝐹 ) )
18		cyclispth	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
19	1	pthhashvtx	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )
20	18 19	syl	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )
21	20	3ad2ant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )
22	4 11 16 17 21	xrltletrd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 2 < ( ♯ ‘ 𝑉 ) )