This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uhgr0v0e

Description: The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020)

Ref Expression
Hypotheses uhgr0v0e.v 
|- V = ( Vtx ` G )
uhgr0v0e.e 
|- E = ( Edg ` G )
Assertion uhgr0v0e 
|- ( ( G e. UHGraph /\ V = (/) ) -> E = (/) )

Proof

Step Hyp Ref Expression
1 uhgr0v0e.v 
 |-  V = ( Vtx ` G )
2 uhgr0v0e.e 
 |-  E = ( Edg ` G )
3 1 eqeq1i 
 |-  ( V = (/) <-> ( Vtx ` G ) = (/) )
4 uhgr0vb 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) )
5 4 biimpd 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph -> ( iEdg ` G ) = (/) ) )
6 5 ex 
 |-  ( G e. UHGraph -> ( ( Vtx ` G ) = (/) -> ( G e. UHGraph -> ( iEdg ` G ) = (/) ) ) )
7 3 6 biimtrid 
 |-  ( G e. UHGraph -> ( V = (/) -> ( G e. UHGraph -> ( iEdg ` G ) = (/) ) ) )
8 7 pm2.43a 
 |-  ( G e. UHGraph -> ( V = (/) -> ( iEdg ` G ) = (/) ) )
9 8 imp 
 |-  ( ( G e. UHGraph /\ V = (/) ) -> ( iEdg ` G ) = (/) )
10 2 eqeq1i 
 |-  ( E = (/) <-> ( Edg ` G ) = (/) )
11 uhgriedg0edg0 
 |-  ( G e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
12 10 11 bitrid 
 |-  ( G e. UHGraph -> ( E = (/) <-> ( iEdg ` G ) = (/) ) )
13 12 adantr 
 |-  ( ( G e. UHGraph /\ V = (/) ) -> ( E = (/) <-> ( iEdg ` G ) = (/) ) )
14 9 13 mpbird 
 |-  ( ( G e. UHGraph /\ V = (/) ) -> E = (/) )