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 eqtrid 
 |-  ( -. 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 =/= (/) ) )