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 )