Theorem acycgr2v

Description: A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023)

	Ref	Expression
Hypothesis	acycgrv.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	acycgr2v	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → 𝐺 ∈ AcyclicGraph )

Proof

Step	Hyp	Ref	Expression
1		acycgrv.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	usgrcyclgt2v	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → 2 < ( ♯ ‘ 𝑉 ) )
3		2re	⊢ 2 ∈ ℝ
4	3	rexri	⊢ 2 ∈ ℝ*
5	1	fvexi	⊢ 𝑉 ∈ V
6		hashxrcl	⊢ ( 𝑉 ∈ V → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
7	5 6	ax-mp	⊢ ( ♯ ‘ 𝑉 ) ∈ ℝ*
8		xrltne	⊢ ( ( 2 ∈ ℝ* ∧ ( ♯ ‘ 𝑉 ) ∈ ℝ* ∧ 2 < ( ♯ ‘ 𝑉 ) ) → ( ♯ ‘ 𝑉 ) ≠ 2 )
9	4 7 8	mp3an12	⊢ ( 2 < ( ♯ ‘ 𝑉 ) → ( ♯ ‘ 𝑉 ) ≠ 2 )
10	9	neneqd	⊢ ( 2 < ( ♯ ‘ 𝑉 ) → ¬ ( ♯ ‘ 𝑉 ) = 2 )
11	2 10	syl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ( ♯ ‘ 𝑉 ) = 2 )
12	11	3expib	⊢ ( 𝐺 ∈ USGraph → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ( ♯ ‘ 𝑉 ) = 2 ) )
13	12	con2d	⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝑉 ) = 2 → ¬ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
14	13	imp	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ¬ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
15	14	nexdv	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ¬ ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
16	15	nexdv	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
17		isacycgr	⊢ ( 𝐺 ∈ USGraph → ( 𝐺 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
18	17	adantr	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( 𝐺 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
19	16 18	mpbird	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → 𝐺 ∈ AcyclicGraph )