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	bilani	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( Vtx ‘ 𝐺 ) = { 𝑣 } )
7		usgr1vr	⊢ ( ( 𝑣 ∈ V ∧ ( Vtx ‘ 𝐺 ) = { 𝑣 } ) → ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )
8	4 6 7	sylancr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )
9	3 8	mpd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( iEdg ‘ 𝐺 ) = ∅ )
10	2	eqeq1i	⊢ ( 𝐸 = ∅ ↔ ( Edg ‘ 𝐺 ) = ∅ )
11		usgruhgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
12		uhgriedg0edg0	⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
13	11 12	syl	⊢ ( 𝐺 ∈ USGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
14	13	adantr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
15	10 14	bitrid	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → ( 𝐸 = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
16	9 15	mpbird	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 = { 𝑣 } ) → 𝐸 = ∅ )
17	16	ex	⊢ ( 𝐺 ∈ USGraph → ( 𝑉 = { 𝑣 } → 𝐸 = ∅ ) )
18	17	exlimdv	⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑣 𝑉 = { 𝑣 } → 𝐸 = ∅ ) )
19	1	fvexi	⊢ 𝑉 ∈ V
20		hash1snb	⊢ ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑣 𝑉 = { 𝑣 } ) )
21	19 20	mp1i	⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑣 𝑉 = { 𝑣 } ) )
22	2	fvexi	⊢ 𝐸 ∈ V
23		hasheq0	⊢ ( 𝐸 ∈ V → ( ( ♯ ‘ 𝐸 ) = 0 ↔ 𝐸 = ∅ ) )
24	22 23	mp1i	⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝐸 ) = 0 ↔ 𝐸 = ∅ ) )
25	18 21 24	3imtr4d	⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝑉 ) = 1 → ( ♯ ‘ 𝐸 ) = 0 ) )
26	25	imp	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ♯ ‘ 𝐸 ) = 0 )