Metamath Proof Explorer


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 syl5bi ( 𝐺 ∈ 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 syl6ibr ( 𝐺 ∈ 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 ) )