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