Metamath Proof Explorer

Theorem acycgr2v

Description: A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 acycgrv.1 
 |-  V = ( Vtx ` G )
2 1 usgrcyclgt2v 
 |-  ( ( G e. USGraph /\ f ( Cycles ` G ) p /\ f =/= (/) ) -> 2 < ( # ` V ) )
3 2re 
 |-  2 e. RR
4 3 rexri 
 |-  2 e. RR*
5 1 fvexi 
 |-  V e. _V
6 hashxrcl 
 |-  ( V e. _V -> ( # ` V ) e. RR* )
7 5 6 ax-mp 
 |-  ( # ` V ) e. RR*
8 xrltne 
 |-  ( ( 2 e. RR* /\ ( # ` V ) e. RR* /\ 2 < ( # ` V ) ) -> ( # ` V ) =/= 2 )
9 4 7 8 mp3an12 
 |-  ( 2 < ( # ` V ) -> ( # ` V ) =/= 2 )
10 9 neneqd 
 |-  ( 2 < ( # ` V ) -> -. ( # ` V ) = 2 )
11 2 10 syl 
 |-  ( ( G e. USGraph /\ f ( Cycles ` G ) p /\ f =/= (/) ) -> -. ( # ` V ) = 2 )
12 11 3expib 
 |-  ( G e. USGraph -> ( ( f ( Cycles ` G ) p /\ f =/= (/) ) -> -. ( # ` V ) = 2 ) )
13 12 con2d 
 |-  ( G e. USGraph -> ( ( # ` V ) = 2 -> -. ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
14 13 imp 
 |-  ( ( G e. USGraph /\ ( # ` V ) = 2 ) -> -. ( f ( Cycles ` G ) p /\ f =/= (/) ) )
15 14 nexdv 
 |-  ( ( G e. USGraph /\ ( # ` V ) = 2 ) -> -. E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
16 15 nexdv 
 |-  ( ( G e. USGraph /\ ( # ` V ) = 2 ) -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
17 isacycgr 
 |-  ( G e. USGraph -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
18 17 adantr 
 |-  ( ( G e. USGraph /\ ( # ` V ) = 2 ) -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
19 16 18 mpbird 
 |-  ( ( G e. USGraph /\ ( # ` V ) = 2 ) -> G e. AcyclicGraph )