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 ⊢V=Vtx⁡G
Assertion cusgracyclt3v ⊢G∈ComplUSGraph→G∈AcyclicGraph↔V<3

Proof

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