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 e. W /\ V = (/) ) -> G e. AcyclicGraph )

Proof

Step Hyp Ref Expression
1 acycgr0v.1 
 |-  V = ( Vtx ` G )
2 br0 
 |-  -. f (/) p
3 df-cycls 
 |-  Cycles = ( g e. _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 >. e. ( Cycles ` G ) )
7 df-br 
 |-  ( f ( Walks ` G ) p <-> <. f , p >. e. ( Walks ` G ) )
8 5 6 7 3imtr3i 
 |-  ( <. f , p >. e. ( Cycles ` G ) -> <. f , p >. e. ( Walks ` G ) )
9 4 8 relssi 
 |-  ( Cycles ` G ) C_ ( 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 ) C_ (/) )
14 ss0 
 |-  ( ( Cycles ` G ) C_ (/) -> ( 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 = (/) -> -. E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
21 20 nexdv 
 |-  ( V = (/) -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
22 isacycgr 
 |-  ( G e. W -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
23 22 biimpar 
 |-  ( ( G e. W /\ -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) -> G e. AcyclicGraph )
24 21 23 sylan2 
 |-  ( ( G e. W /\ V = (/) ) -> G e. AcyclicGraph )