Metamath Proof Explorer

Theorem usgr1v0e

Description: The size of a (finite) simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 22-Oct-2020)

Ref Expression
Hypotheses fusgredgfi.v 
|- V = ( Vtx ` G )
fusgredgfi.e 
|- E = ( Edg ` G )
Assertion usgr1v0e 
|- ( ( G e. USGraph /\ ( # ` V ) = 1 ) -> ( # ` E ) = 0 )

Proof

Step Hyp Ref Expression
1 fusgredgfi.v 
 |-  V = ( Vtx ` G )
2 fusgredgfi.e 
 |-  E = ( Edg ` G )
3 simpl 
 |-  ( ( G e. USGraph /\ V = { v } ) -> G e. USGraph )
4 vex 
 |-  v e. _V
5 1 eqeq1i 
 |-  ( V = { v } <-> ( Vtx ` G ) = { v } )
6 5 biimpi 
 |-  ( V = { v } -> ( Vtx ` G ) = { v } )
7 6 adantl 
 |-  ( ( G e. USGraph /\ V = { v } ) -> ( Vtx ` G ) = { v } )
8 usgr1vr 
 |-  ( ( v e. _V /\ ( Vtx ` G ) = { v } ) -> ( G e. USGraph -> ( iEdg ` G ) = (/) ) )
9 4 7 8 sylancr 
 |-  ( ( G e. USGraph /\ V = { v } ) -> ( G e. USGraph -> ( iEdg ` G ) = (/) ) )
10 3 9 mpd 
 |-  ( ( G e. USGraph /\ V = { v } ) -> ( iEdg ` G ) = (/) )
11 2 eqeq1i 
 |-  ( E = (/) <-> ( Edg ` G ) = (/) )
12 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
13 uhgriedg0edg0 
 |-  ( G e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
14 12 13 syl 
 |-  ( G e. USGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
15 14 adantr 
 |-  ( ( G e. USGraph /\ V = { v } ) -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
16 11 15 bitrid 
 |-  ( ( G e. USGraph /\ V = { v } ) -> ( E = (/) <-> ( iEdg ` G ) = (/) ) )
17 10 16 mpbird 
 |-  ( ( G e. USGraph /\ V = { v } ) -> E = (/) )
18 17 ex 
 |-  ( G e. USGraph -> ( V = { v } -> E = (/) ) )
19 18 exlimdv 
 |-  ( G e. USGraph -> ( E. v V = { v } -> E = (/) ) )
20 1 fvexi 
 |-  V e. _V
21 hash1snb 
 |-  ( V e. _V -> ( ( # ` V ) = 1 <-> E. v V = { v } ) )
22 20 21 mp1i 
 |-  ( G e. USGraph -> ( ( # ` V ) = 1 <-> E. v V = { v } ) )
23 2 fvexi 
 |-  E e. _V
24 hasheq0 
 |-  ( E e. _V -> ( ( # ` E ) = 0 <-> E = (/) ) )
25 23 24 mp1i 
 |-  ( G e. USGraph -> ( ( # ` E ) = 0 <-> E = (/) ) )
26 19 22 25 3imtr4d 
 |-  ( G e. USGraph -> ( ( # ` V ) = 1 -> ( # ` E ) = 0 ) )
27 26 imp 
 |-  ( ( G e. USGraph /\ ( # ` V ) = 1 ) -> ( # ` E ) = 0 )