Theorem usgr0vb

Description: The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017) (Revised by AV, 16-Oct-2020)

	Ref	Expression
Assertion	usgr0vb	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		usgruhgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
2		uhgr0vb	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
3	1 2	imbitrid	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )
4		simpl	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ 𝑊 )
5		simpr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ )
6	4 5	usgr0e	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )
7	6	ex	⊢ ( 𝐺 ∈ 𝑊 → ( ( iEdg ‘ 𝐺 ) = ∅ → 𝐺 ∈ USGraph ) )
8	7	adantr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( iEdg ‘ 𝐺 ) = ∅ → 𝐺 ∈ USGraph ) )
9	3 8	impbid	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )