Metamath Proof Explorer

Theorem acycgr1v

Description: A multigraph with one vertex is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023)

Ref Expression
Hypothesis acycgrv.1 
|- V = ( Vtx ` G )
Assertion acycgr1v 
|- ( ( G e. UMGraph /\ ( # ` V ) = 1 ) -> G e. AcyclicGraph )

Proof

Step Hyp Ref Expression
1 acycgrv.1 
 |-  V = ( Vtx ` G )
2 cyclispth 
 |-  ( f ( Cycles ` G ) p -> f ( Paths ` G ) p )
3 1 pthhashvtx 
 |-  ( f ( Paths ` G ) p -> ( # ` f ) <_ ( # ` V ) )
4 2 3 syl 
 |-  ( f ( Cycles ` G ) p -> ( # ` f ) <_ ( # ` V ) )
5 4 adantr 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( # ` f ) <_ ( # ` V ) )
6 breq2 
 |-  ( ( # ` V ) = 1 -> ( ( # ` f ) <_ ( # ` V ) <-> ( # ` f ) <_ 1 ) )
7 6 adantl 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( ( # ` f ) <_ ( # ` V ) <-> ( # ` f ) <_ 1 ) )
8 5 7 mpbid 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( # ` f ) <_ 1 )
9 8 3adant1 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( # ` f ) <_ 1 )
10 umgrn1cycl 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p ) -> ( # ` f ) =/= 1 )
11 10 3adant3 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( # ` f ) =/= 1 )
12 11 necomd 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> 1 =/= ( # ` f ) )
13 cycliswlk 
 |-  ( f ( Cycles ` G ) p -> f ( Walks ` G ) p )
14 wlkcl 
 |-  ( f ( Walks ` G ) p -> ( # ` f ) e. NN0 )
15 14 nn0red 
 |-  ( f ( Walks ` G ) p -> ( # ` f ) e. RR )
16 1red 
 |-  ( f ( Walks ` G ) p -> 1 e. RR )
17 15 16 ltlend 
 |-  ( f ( Walks ` G ) p -> ( ( # ` f ) < 1 <-> ( ( # ` f ) <_ 1 /\ 1 =/= ( # ` f ) ) ) )
18 13 17 syl 
 |-  ( f ( Cycles ` G ) p -> ( ( # ` f ) < 1 <-> ( ( # ` f ) <_ 1 /\ 1 =/= ( # ` f ) ) ) )
19 18 3ad2ant2 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( ( # ` f ) < 1 <-> ( ( # ` f ) <_ 1 /\ 1 =/= ( # ` f ) ) ) )
20 9 12 19 mpbir2and 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( # ` f ) < 1 )
21 nn0lt10b 
 |-  ( ( # ` f ) e. NN0 -> ( ( # ` f ) < 1 <-> ( # ` f ) = 0 ) )
22 13 14 21 3syl 
 |-  ( f ( Cycles ` G ) p -> ( ( # ` f ) < 1 <-> ( # ` f ) = 0 ) )
23 22 3ad2ant2 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( ( # ` f ) < 1 <-> ( # ` f ) = 0 ) )
24 20 23 mpbid 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> ( # ` f ) = 0 )
25 hasheq0 
 |-  ( f e. _V -> ( ( # ` f ) = 0 <-> f = (/) ) )
26 25 elv 
 |-  ( ( # ` f ) = 0 <-> f = (/) )
27 24 26 sylib 
 |-  ( ( G e. UMGraph /\ f ( Cycles ` G ) p /\ ( # ` V ) = 1 ) -> f = (/) )
28 27 3com23 
 |-  ( ( G e. UMGraph /\ ( # ` V ) = 1 /\ f ( Cycles ` G ) p ) -> f = (/) )
29 28 3expia 
 |-  ( ( G e. UMGraph /\ ( # ` V ) = 1 ) -> ( f ( Cycles ` G ) p -> f = (/) ) )
30 29 alrimivv 
 |-  ( ( G e. UMGraph /\ ( # ` V ) = 1 ) -> A. f A. p ( f ( Cycles ` G ) p -> f = (/) ) )
31 isacycgr1 
 |-  ( G e. UMGraph -> ( G e. AcyclicGraph <-> A. f A. p ( f ( Cycles ` G ) p -> f = (/) ) ) )
32 31 adantr 
 |-  ( ( G e. UMGraph /\ ( # ` V ) = 1 ) -> ( G e. AcyclicGraph <-> A. f A. p ( f ( Cycles ` G ) p -> f = (/) ) ) )
33 30 32 mpbird 
 |-  ( ( G e. UMGraph /\ ( # ` V ) = 1 ) -> G e. AcyclicGraph )