Metamath Proof Explorer

Theorem usgr1vr

Description: A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 2-Apr-2021)

Ref Expression
Assertion usgr1vr 
|- ( ( A e. X /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph -> ( iEdg ` G ) = (/) ) )

Proof

Step Hyp Ref Expression
1 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
2 1 adantl 
 |-  ( ( ( A e. X /\ ( Vtx ` G ) = { A } ) /\ G e. USGraph ) -> G e. UHGraph )
3 fveq2 
 |-  ( ( Vtx ` G ) = { A } -> ( # ` ( Vtx ` G ) ) = ( # ` { A } ) )
4 hashsng 
 |-  ( A e. X -> ( # ` { A } ) = 1 )
5 3 4 sylan9eqr 
 |-  ( ( A e. X /\ ( Vtx ` G ) = { A } ) -> ( # ` ( Vtx ` G ) ) = 1 )
6 5 adantr 
 |-  ( ( ( A e. X /\ ( Vtx ` G ) = { A } ) /\ G e. USGraph ) -> ( # ` ( Vtx ` G ) ) = 1 )
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
9 7 8 usgrislfuspgr 
 |-  ( G e. USGraph <-> ( G e. USPGraph /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } ) )
10 9 simprbi 
 |-  ( G e. USGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } )
11 10 adantl 
 |-  ( ( ( A e. X /\ ( Vtx ` G ) = { A } ) /\ G e. USGraph ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } )
12 eqid 
 |-  { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } = { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) }
13 7 8 12 lfuhgr1v0e 
 |-  ( ( G e. UHGraph /\ ( # ` ( Vtx ` G ) ) = 1 /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } ) -> ( Edg ` G ) = (/) )
14 2 6 11 13 syl3anc 
 |-  ( ( ( A e. X /\ ( Vtx ` G ) = { A } ) /\ G e. USGraph ) -> ( Edg ` G ) = (/) )
15 uhgriedg0edg0 
 |-  ( G e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
16 1 15 syl 
 |-  ( G e. USGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
17 16 adantl 
 |-  ( ( ( A e. X /\ ( Vtx ` G ) = { A } ) /\ G e. USGraph ) -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
18 14 17 mpbid 
 |-  ( ( ( A e. X /\ ( Vtx ` G ) = { A } ) /\ G e. USGraph ) -> ( iEdg ` G ) = (/) )
19 18 ex 
 |-  ( ( A e. X /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph -> ( iEdg ` G ) = (/) ) )