Metamath Proof Explorer


Theorem prclisacycgr

Description: A proper class (representing a null graph, see vtxvalprc ) has the property of an acyclic graph (see also acycgr0v ). (Contributed by BTernaryTau, 11-Oct-2023) (New usage is discouraged.)

Ref Expression
Hypothesis prclisacycgr.1 V = Vtx G
Assertion prclisacycgr ¬ G V ¬ f p f Cycles G p f

Proof

Step Hyp Ref Expression
1 prclisacycgr.1 V = Vtx G
2 fvprc ¬ G V Vtx G =
3 1 2 syl5eq ¬ G V V =
4 br0 ¬ f p
5 df-cycls Cycles = g V f p | f Paths g p p 0 = p f
6 5 relmptopab Rel Cycles G
7 cycliswlk f Cycles G p f Walks G p
8 df-br f Cycles G p f p Cycles G
9 df-br f Walks G p f p Walks G
10 7 8 9 3imtr3i f p Cycles G f p Walks G
11 6 10 relssi Cycles G Walks G
12 1 eqeq1i V = Vtx G =
13 g0wlk0 Vtx G = Walks G =
14 12 13 sylbi V = Walks G =
15 11 14 sseqtrid V = Cycles G
16 ss0 Cycles G Cycles G =
17 breq Cycles G = f Cycles G p f p
18 17 notbid Cycles G = ¬ f Cycles G p ¬ f p
19 15 16 18 3syl V = ¬ f Cycles G p ¬ f p
20 4 19 mpbiri V = ¬ f Cycles G p
21 20 intnanrd V = ¬ f Cycles G p f
22 21 nexdv V = ¬ p f Cycles G p f
23 22 nexdv V = ¬ f p f Cycles G p f
24 3 23 syl ¬ G V ¬ f p f Cycles G p f