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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	fusgredgfi.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	usgr1v0e	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ♯ ‘ 𝐸 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		fusgredgfi.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgredgfi.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		simpl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → 𝐺 ∈ USGraph )
4		vex	⊢ 𝑣 ∈ V
5	1	eqeq1i	⊢ ( 𝑉 = { 𝑣 } ↔ ( Vtx ‘ 𝐺 ) = { 𝑣 } )
6	5	biimpi	⊢ ( 𝑉 = { 𝑣 } → ( Vtx ‘ 𝐺 ) = { 𝑣 } )
7	6	adantl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( Vtx ‘ 𝐺 ) = { 𝑣 } )
8		usgr1vr	⊢ ( ( 𝑣 ∈ V ∧ ( Vtx ‘ 𝐺 ) = { 𝑣 } ) → ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )
9	4 7 8	sylancr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )
10	3 9	mpd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( iEdg ‘ 𝐺 ) = ∅ )
11	2	eqeq1i	⊢ ( 𝐸 = ∅ ↔ ( Edg ‘ 𝐺 ) = ∅ )
12		usgruhgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
13		uhgriedg0edg0	⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
14	12 13	syl	⊢ ( 𝐺 ∈ USGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
15	14	adantr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
16	11 15	bitrid	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( 𝐸 = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
17	10 16	mpbird	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → 𝐸 = ∅ )
18	17	ex	⊢ ( 𝐺 ∈ USGraph → ( 𝑉 = { 𝑣 } → 𝐸 = ∅ ) )
19	18	exlimdv	⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑣 𝑉 = { 𝑣 } → 𝐸 = ∅ ) )
20	1	fvexi	⊢ 𝑉 ∈ V
21		hash1snb	⊢ ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑣 𝑉 = { 𝑣 } ) )
22	20 21	mp1i	⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑣 𝑉 = { 𝑣 } ) )
23	2	fvexi	⊢ 𝐸 ∈ V
24		hasheq0	⊢ ( 𝐸 ∈ V → ( ( ♯ ‘ 𝐸 ) = 0 ↔ 𝐸 = ∅ ) )
25	23 24	mp1i	⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝐸 ) = 0 ↔ 𝐸 = ∅ ) )
26	19 22 25	3imtr4d	⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝑉 ) = 1 → ( ♯ ‘ 𝐸 ) = 0 ) )
27	26	imp	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ♯ ‘ 𝐸 ) = 0 )