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 e. _V -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )

Proof

Step Hyp Ref Expression
1 prclisacycgr.1
 |-  V = ( Vtx ` G )
2 fvprc
 |-  ( -. G e. _V -> ( Vtx ` G ) = (/) )
3 1 2 syl5eq
 |-  ( -. G e. _V -> V = (/) )
4 br0
 |-  -. f (/) p
5 df-cycls
 |-  Cycles = ( g e. _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 >. e. ( Cycles ` G ) )
9 df-br
 |-  ( f ( Walks ` G ) p <-> <. f , p >. e. ( Walks ` G ) )
10 7 8 9 3imtr3i
 |-  ( <. f , p >. e. ( Cycles ` G ) -> <. f , p >. e. ( Walks ` G ) )
11 6 10 relssi
 |-  ( Cycles ` G ) C_ ( 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 ) C_ (/) )
16 ss0
 |-  ( ( Cycles ` G ) C_ (/) -> ( 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 = (/) -> -. E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
23 22 nexdv
 |-  ( V = (/) -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
24 3 23 syl
 |-  ( -. G e. _V -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )