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