Metamath Proof Explorer

Theorem acycgr0v

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

Ref Expression
Hypothesis acycgr0v.1 ⊢ V = Vtx ⁡ G
Assertion acycgr0v ⊢ G ∈ W ∧ V = ∅ → G ∈ AcyclicGraph

Proof

Step Hyp Ref Expression
1 acycgr0v.1 ⊢ V = Vtx ⁡ G
2 br0 ⊢ ¬ f ∅ p
3 df-cycls ⊢ Cycles = g ∈ V ⟼ f p | f Paths ⁡ g p ∧ p ⁡ 0 = p ⁡ f
4 3 relmptopab ⊢ Rel ⁡ Cycles ⁡ G
5 cycliswlk ⊢ f Cycles ⁡ G p → f Walks ⁡ G p
6 df-br ⊢ f Cycles ⁡ G p ↔ f p ∈ Cycles ⁡ G
7 df-br ⊢ f Walks ⁡ G p ↔ f p ∈ Walks ⁡ G
8 5 6 7 3imtr3i ⊢ f p ∈ Cycles ⁡ G → f p ∈ Walks ⁡ G
9 4 8 relssi ⊢ Cycles ⁡ G ⊆ Walks ⁡ G
10 1 eqeq1i ⊢ V = ∅ ↔ Vtx ⁡ G = ∅
11 g0wlk0 ⊢ Vtx ⁡ G = ∅ → Walks ⁡ G = ∅
12 10 11 sylbi ⊢ V = ∅ → Walks ⁡ G = ∅
13 9 12 sseqtrid ⊢ V = ∅ → Cycles ⁡ G ⊆ ∅
14 ss0 ⊢ Cycles ⁡ G ⊆ ∅ → Cycles ⁡ G = ∅
15 breq ⊢ Cycles ⁡ G = ∅ → f Cycles ⁡ G p ↔ f ∅ p
16 15 notbid ⊢ Cycles ⁡ G = ∅ → ¬ f Cycles ⁡ G p ↔ ¬ f ∅ p
17 13 14 16 3syl ⊢ V = ∅ → ¬ f Cycles ⁡ G p ↔ ¬ f ∅ p
18 2 17 mpbiri ⊢ V = ∅ → ¬ f Cycles ⁡ G p
19 18 intnanrd ⊢ V = ∅ → ¬ f Cycles ⁡ G p ∧ f ≠ ∅
20 19 nexdv ⊢ V = ∅ → ¬ ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
21 20 nexdv ⊢ V = ∅ → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
22 isacycgr ⊢ G ∈ W → G ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
23 22 biimpar ⊢ G ∈ W ∧ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅ → G ∈ AcyclicGraph
24 21 23 sylan2 ⊢ G ∈ W ∧ V = ∅ → G ∈ AcyclicGraph