Theorem uhgr0vusgr

Description: The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020)

	Ref	Expression
Assertion	uhgr0vusgr	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ UHGraph )
2		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4	2 3	uhgr0v0e	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( Edg ‘ 𝐺 ) = ∅ )
5		uhgriedg0edg0	⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
6	5	adantr	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
7	4 6	mpbid	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ )
8	1 7	usgr0e	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )