Metamath Proof Explorer


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
|- ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> G e. UHGraph )
2 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid
 |-  ( Edg ` G ) = ( Edg ` G )
4 2 3 uhgr0v0e
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( Edg ` G ) = (/) )
5 uhgriedg0edg0
 |-  ( G e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
6 5 adantr
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
7 4 6 mpbid
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
8 1 7 usgr0e
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> G e. USGraph )