Theorem cusgracyclt3v

Description: A complete simple graph is acyclic if and only if it has fewer than three vertices. (Contributed by BTernaryTau, 20-Oct-2023)

	Ref	Expression
Hypothesis	cusgracyclt3v.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	cusgracyclt3v	⊢ ( 𝐺 ∈ ComplUSGraph → ( 𝐺 ∈ AcyclicGraph ↔ ( ♯ ‘ 𝑉 ) < 3 ) )

Proof

Step	Hyp	Ref	Expression
1		cusgracyclt3v.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isacycgr	⊢ ( 𝐺 ∈ ComplUSGraph → ( 𝐺 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
3		3nn0	⊢ 3 ∈ ℕ0
4	1	fvexi	⊢ 𝑉 ∈ V
5		hashxnn0	⊢ ( 𝑉 ∈ V → ( ♯ ‘ 𝑉 ) ∈ ℕ0* )
6	4 5	ax-mp	⊢ ( ♯ ‘ 𝑉 ) ∈ ℕ0*
7		xnn0lem1lt	⊢ ( ( 3 ∈ ℕ0 ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0* ) → ( 3 ≤ ( ♯ ‘ 𝑉 ) ↔ ( 3 − 1 ) < ( ♯ ‘ 𝑉 ) ) )
8	3 6 7	mp2an	⊢ ( 3 ≤ ( ♯ ‘ 𝑉 ) ↔ ( 3 − 1 ) < ( ♯ ‘ 𝑉 ) )
9		3re	⊢ 3 ∈ ℝ
10	9	rexri	⊢ 3 ∈ ℝ*
11		xnn0xr	⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0* → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
12	6 11	ax-mp	⊢ ( ♯ ‘ 𝑉 ) ∈ ℝ*
13		xrlenlt	⊢ ( ( 3 ∈ ℝ* ∧ ( ♯ ‘ 𝑉 ) ∈ ℝ* ) → ( 3 ≤ ( ♯ ‘ 𝑉 ) ↔ ¬ ( ♯ ‘ 𝑉 ) < 3 ) )
14	10 12 13	mp2an	⊢ ( 3 ≤ ( ♯ ‘ 𝑉 ) ↔ ¬ ( ♯ ‘ 𝑉 ) < 3 )
15		3m1e2	⊢ ( 3 − 1 ) = 2
16	15	breq1i	⊢ ( ( 3 − 1 ) < ( ♯ ‘ 𝑉 ) ↔ 2 < ( ♯ ‘ 𝑉 ) )
17	8 14 16	3bitr3i	⊢ ( ¬ ( ♯ ‘ 𝑉 ) < 3 ↔ 2 < ( ♯ ‘ 𝑉 ) )
18	1	cusgr3cyclex	⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 2 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
19		3ne0	⊢ 3 ≠ 0
20		neeq1	⊢ ( ( ♯ ‘ 𝑓 ) = 3 → ( ( ♯ ‘ 𝑓 ) ≠ 0 ↔ 3 ≠ 0 ) )
21	19 20	mpbiri	⊢ ( ( ♯ ‘ 𝑓 ) = 3 → ( ♯ ‘ 𝑓 ) ≠ 0 )
22		hasheq0	⊢ ( 𝑓 ∈ V → ( ( ♯ ‘ 𝑓 ) = 0 ↔ 𝑓 = ∅ ) )
23	22	elv	⊢ ( ( ♯ ‘ 𝑓 ) = 0 ↔ 𝑓 = ∅ )
24	23	necon3bii	⊢ ( ( ♯ ‘ 𝑓 ) ≠ 0 ↔ 𝑓 ≠ ∅ )
25	21 24	sylib	⊢ ( ( ♯ ‘ 𝑓 ) = 3 → 𝑓 ≠ ∅ )
26	25	anim2i	⊢ ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
27	26	2eximi	⊢ ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
28	18 27	syl	⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 2 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
29	28	ex	⊢ ( 𝐺 ∈ ComplUSGraph → ( 2 < ( ♯ ‘ 𝑉 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
30	17 29	biimtrid	⊢ ( 𝐺 ∈ ComplUSGraph → ( ¬ ( ♯ ‘ 𝑉 ) < 3 → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
31	30	con1d	⊢ ( 𝐺 ∈ ComplUSGraph → ( ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ( ♯ ‘ 𝑉 ) < 3 ) )
32	2 31	sylbid	⊢ ( 𝐺 ∈ ComplUSGraph → ( 𝐺 ∈ AcyclicGraph → ( ♯ ‘ 𝑉 ) < 3 ) )
33		cusgrusgr	⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph )
34	1	usgrcyclgt2v	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → 2 < ( ♯ ‘ 𝑉 ) )
35	34	3expib	⊢ ( 𝐺 ∈ USGraph → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → 2 < ( ♯ ‘ 𝑉 ) ) )
36	33 35	syl	⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → 2 < ( ♯ ‘ 𝑉 ) ) )
37	36 17	imbitrrdi	⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ( ♯ ‘ 𝑉 ) < 3 ) )
38	37	exlimdvv	⊢ ( 𝐺 ∈ ComplUSGraph → ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ( ♯ ‘ 𝑉 ) < 3 ) )
39	38	con2d	⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝑉 ) < 3 → ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
40	39 2	sylibrd	⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝑉 ) < 3 → 𝐺 ∈ AcyclicGraph ) )
41	32 40	impbid	⊢ ( 𝐺 ∈ ComplUSGraph → ( 𝐺 ∈ AcyclicGraph ↔ ( ♯ ‘ 𝑉 ) < 3 ) )