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

Metamath Proof Explorer

Theorem vtxduhgr0edgnel

Description: A vertex in a hypergraph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v 
|- V = ( Vtx ` G )
vtxdushgrfvedg.e 
|- E = ( Edg ` G )
vtxdushgrfvedg.d 
|- D = ( VtxDeg ` G )
Assertion vtxduhgr0edgnel 
|- ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v 
 |-  V = ( Vtx ` G )
2 vtxdushgrfvedg.e 
 |-  E = ( Edg ` G )
3 vtxdushgrfvedg.d 
 |-  D = ( VtxDeg ` G )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 1 4 3 vtxd0nedgb 
 |-  ( U e. V -> ( ( D ` U ) = 0 <-> -. E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) ) )
6 5 adantl 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) ) )
7 4 2 uhgrvtxedgiedgb 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) <-> E. e e. E U e. e ) )
8 7 notbid 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( -. E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) <-> -. E. e e. E U e. e ) )
9 6 8 bitrd 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )