Theorem acycgr0v

Description: A null graph (with no vertices) is an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023)

	Ref	Expression
Hypothesis	acycgr0v.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	acycgr0v	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ) → 𝐺 ∈ AcyclicGraph )

Proof

Step	Hyp	Ref	Expression
1		acycgr0v.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		br0	⊢ ¬ 𝑓 ∅ 𝑝
3		df-cycls	⊢ Cycles = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } )
4	3	relmptopab	⊢ Rel ( Cycles ‘ 𝐺 )
5		cycliswlk	⊢ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
6		df-br	⊢ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ⟨ 𝑓 , 𝑝 ⟩ ∈ ( Cycles ‘ 𝐺 ) )
7		df-br	⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ ⟨ 𝑓 , 𝑝 ⟩ ∈ ( Walks ‘ 𝐺 ) )
8	5 6 7	3imtr3i	⊢ ( ⟨ 𝑓 , 𝑝 ⟩ ∈ ( Cycles ‘ 𝐺 ) → ⟨ 𝑓 , 𝑝 ⟩ ∈ ( Walks ‘ 𝐺 ) )
9	4 8	relssi	⊢ ( Cycles ‘ 𝐺 ) ⊆ ( Walks ‘ 𝐺 )
10	1	eqeq1i	⊢ ( 𝑉 = ∅ ↔ ( Vtx ‘ 𝐺 ) = ∅ )
11		g0wlk0	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ )
12	10 11	sylbi	⊢ ( 𝑉 = ∅ → ( Walks ‘ 𝐺 ) = ∅ )
13	9 12	sseqtrid	⊢ ( 𝑉 = ∅ → ( Cycles ‘ 𝐺 ) ⊆ ∅ )
14		ss0	⊢ ( ( Cycles ‘ 𝐺 ) ⊆ ∅ → ( Cycles ‘ 𝐺 ) = ∅ )
15		breq	⊢ ( ( Cycles ‘ 𝐺 ) = ∅ → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ 𝑓 ∅ 𝑝 ) )
16	15	notbid	⊢ ( ( Cycles ‘ 𝐺 ) = ∅ → ( ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ¬ 𝑓 ∅ 𝑝 ) )
17	13 14 16	3syl	⊢ ( 𝑉 = ∅ → ( ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ¬ 𝑓 ∅ 𝑝 ) )
18	2 17	mpbiri	⊢ ( 𝑉 = ∅ → ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 )
19	18	intnanrd	⊢ ( 𝑉 = ∅ → ¬ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
20	19	nexdv	⊢ ( 𝑉 = ∅ → ¬ ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
21	20	nexdv	⊢ ( 𝑉 = ∅ → ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
22		isacycgr	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
23	22	biimpar	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) → 𝐺 ∈ AcyclicGraph )
24	21 23	sylan2	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ) → 𝐺 ∈ AcyclicGraph )